We are very much trying to not dump things in various...

For what it's worth, this is not shared by all core developers; personally I feel that the Preferences dialog already has loads of options and that it's better for preferences that are obscure or rarely used to be dumped into the Various preferences tab. In any case, I don't feel strongly, I just mention so it's clear this is not some kind of agreed upon policy. IMO, leave it to the person willing to make the PR, it can always be moved later if it turns out people are using it a lot for some reason or having trouble finding it.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.