Ignacio wrote, re. changing the gretl menu font independently
of the system menu font on Windows:
> It is rather practical when you are using a proyector for
example, for
> teaching, because this allows to enlarge the font or put it in bold for
> better viewing.
OK, I have now reinstated the old behavior on Windows. That
is, you get a working selector for the menu font if and only
if you have deselected "Emulate Windows look" under general
preferences.
It may be possible to support menu font selection even when
emulation of the "Windows look" is in force (which looks very
much better on recent Windows), but I haven't yet found a way
of doing that.
Allin