When configuring the editor, it's useful to have everything "in reach", instead of looking around in menus (you can't even click on menus while the preferences are opened).
...
For example, with the 'hide fold margin' option, if you wanted to quickly enable/disable it

Good points. So then that's another criterion to decide on whether it goes into "View" menu, vs in "Preferences" and/or configuration files. (My motivation is just to reduce unnecessary duplication/visual noise in various settings' location )
Like, is 'hide fold margin' something you would want to change often ?
Personally, I'd decide early on whether I want to hide it or not, set it so, and very rarely need to change it again.

Anyway, it's a relatively minor point, thanks again for implementing.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.
Triage notifications on the go with GitHub Mobile for iOS or Android.