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