Changing WinHugs font size

Markus L. Noga markus@noga.de
Fri, 18 Oct 2002 10:10:27 +0200


Hello,

how does one go about changing the font size in WinHugs? Please reply by
mail, as I do not subscribe to this list.

Kind regards,
      Markus L. Noga

---
Markus L. Noga <markus@noga.de>
Program Structures Group
Universit=E4t Karlsruhe=20