Subject: bug#22000: Patch addressing the menu-bar frame-resize interaction

From: Vivek Dasmohapatra <[email-masked]>
Date: Fri, 12 Oct 2018 19:16:17 +0100 (BST)

> for users who want the resize problem get fixed and who are willing to
> pay for that with a higher menu bar.  And one option value (say
> 'resize') for users who can live with the resizing problem but care more
> about the height of the menu bar.

I've used a CSS provider to strip away all the extra space. I have to put
a little bit back to prevent a UI focus bug when the scrollbar is present
but it's still a lot more compact than it was: Attached screenshot shows
new / new+scrollbar / old - as you can see new w/o scrollbars is the same
height as old.