Such a plugin already exist (though seems abandoned) as mentioned in #633. This could probably be used as a base.
Or, as @elextr suggested, have a look at the Addons plugin. Adding a new shortcut there to show/hide the menu bar is probably no big deal, is less work than creating a whole new plugin with all boilerplate and has good chances to be merged.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.