Font size in Hugs for Macintosh
11 Oct
2001
11 Oct
'01
10:14 a.m.
Hi, 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? Thanks, Matthias
12 Oct
12 Oct
10:39 p.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
8851
Age (days ago)
8852
Last active (days ago)
1 comments
2 participants
participants (2)
-
Hans Aberg -
Matthias Mann