On Thu, 23 Oct 2014, Artur T. wrote:
Ok, I just realized after re-opening gretl, that the font changes for
the
script editor now, whereas for the command line this happens instantly
without need to re-open gretl. Maybe one could give a message that changes
apply after re-opening gretl.
Not even that. All you have to do is close the window and reopen it.
-------------------------------------------------------
Riccardo (Jack) Lucchetti
Dipartimento di Scienze Economiche e Sociali (DiSES)
Università Politecnica delle Marche
(formerly known as Università di Ancona)
r.lucchetti(a)univpm.it
http://www2.econ.univpm.it/servizi/hpp/lucchetti
-------------------------------------------------------