[Gretl-devel] font size script editor and main window

Dear gretl developers, I just realized that it is not possible to change the font size of the script editor as well as gretl main window. We use gretl for teaching purposes and beam gretl at the wall. However, for students sitting in the back of the classroom the font size is always too small. At least using the Windows version (built 9. Sept. 2014) the font change using the option "Fixed font" does only refer to the command line but not the script editor. Of ourse we could always use antoher editor for this but I thought it should be possible to change the font size inside gretl as well. Best, Artur