@elextr The menubar state is not saved and restored. The option to hide on startup is kept because that is the behavior I expect most users who would hide the menu bar would want. I will update the initial description.

Discussions should preferably happen before implemention so it only has to be done once.

Too much discussion, and it may be several years before implementation. A concrete implementation can bring up issues that might not come up otherwise. There's no guarantee that an implementation with lots of discussion won't need to be revised.


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.