Scroll-bars used to draw in a little extra space in the editor, causing buttons to jump a bit when they appeared/disappeared. Now they draw on top of the buttons, just small enough to avoid bigger overlaps. Followup commits will do further adjustments. With this we can get rid of a hack that was calling the (often Python defined) panel definition - the panel 'draw' callback - twice.
63 KiB
63 KiB