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