Expected behavior
Different tabs in Workbench editor should display in the same font size
Actual behavior
DIfferent tabs in Workbench have different font size
Steps to reproduce the behaviour
- Open workbench, the editor by default opens an empty script, with a given font size (quite large my case.
- Click the + to open a new tab. The new tab has a significantly larger font size, far too large to use.
- Third or fourth tabs have the same font size as the second tab
- If I use command-(+/-) to rescale the font size, all tabs scale by the same amount. So, when I get tab 2 (+3,4 etc) to the correct size, tab 1 is illegibly small.
Platforms affected
I’ve only tested this on my 2018 macbook pro, running Catalina 10.15.5. It’s the same on both the native retina and when I connect an external screen. I’m running mantid 5.0.0.