Spoofax font size should set in normal Eclipse settings
Changing the font size for editors is currently done in IMP-specific settings. This should be integrated directly in Eclipse’s font settings.
Submitted by Vlad Vergu on 14 December 2012 at 15:10
Issue Log
On 14 December 2012 at 16:48 Gabriël Konat commented:
Changing the Eclipse default font size also works, but is only applied to open IMP editors. Eclipse has to be restarted to apply it to new editors.
On 18 December 2012 at 14:14 Gabriël Konat tagged imp
On 8 January 2013 at 13:09 Eelco Visser tagged imp
On 10 March 2013 at 11:57 Guido Wachsmuth tagged eclipse
Log in to post comments