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
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.
Log in to post comments