13 Oct
2001
13 Oct
'01
4:09 a.m.
At 12:14 +0200 2001/10/11, Matthias Mann wrote:
I just wonder whether it's possible to change the size of the font in the interpreter window of Hugs on the Mac. Does anybody have an idea how to do this? Or is the only possibility to switch between certain screen resolutions?
I made an update to the version that I and Pablo Azero used to develop; see the next email for info. Hans Aberg