Re: Font size in Hugs for Macintosh

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