[GREENFOOT-435] Editor preferences need rethinking
The editor preference pane currently applies to the Java editor only.
We either need another one for the Stride editor, or two sections in the editor pref pane \- maybe the font size should apply to both.
In any case, there should be a numerical preference setting for font size in preferences that applies to the Stride editor.
Issue metadata
- Issue type: Task
- Priority: Low