So I don't have an opinion on whether folding should be allowed to be disabled or not, but currently it is, so I've implemented the new feature for all cases.. But, if you wanted to go ahead and remove the option to disable folding in the future, being able to hide the margin would satisfy those that do not use/want it.
On personal opinion level, since it's been mentioned here, I think the duplication of some items in the menu and the preferences dialog is ok. For example, with the 'hide fold margin' option, if you wanted to quickly enable/disable it, you would have to go through the not-necessarily-too-quick preferences dialog (if it was there only). 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). I will look into updating the manual. -- You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub: https://github.com/geany/geany/pull/2927#issuecomment-940183703
