Closed DamienCassou closed 2 years ago
Thanks, I should have changed the name when I change it from a defvar to a custom option. Merged. :-)
Doesn't look like you did :-).
yeah I merged locally and made a new version and though I probably shouldn't make a new version before settling on all the changes and don't want to push it before all pr's are closed and set but you can't see the change without I push so yeah I probably should have just pushed it :-) I pushed it.
thank you. I'm closing the PR.
Symbols starting vundo-- should be kept for private use which is not the case of a user option such as vundo--window-max-height.