[BLUEJ-503] Editor font size only affects terminal font size after restarting BlueJ
If the editor font size is changed, the terminal font size is not changed until BlueJ is closed and restarted. It is documented that it should change to match the editor if not otherwise specified in bluej.defs.
Looking at the source, it would appear that a call to setTerminalFontSize() in PrefMgr.setEditorFontSize() would fix this.
(Also, ticket BLUEJ-166 notes that Ctrl+ and Ctrl= have been added to change the font size, but this does not appear to be mentioned anywhere in the documentation since this fix was made.)
Issue metadata
- Issue type: Bug
- Priority: Medium
- Fix versions: 3.1.6