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

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