Gui: Change font to Fixed in options dialog
commit85d3b7769786d58d2341d8ef05c3753cec416b80
authorAdam Folmert <afolmert@gmail.com>
Mon, 21 Apr 2008 14:02:19 +0000 (21 10:02 -0400)
committerAdam Folmert <afolmert@gmail.com>
Mon, 21 Apr 2008 14:02:19 +0000 (21 10:02 -0400)
tree8a258a54a7baea0f5af53a40e5fc4345610ef780
parent523ad0b37e00d38b361e0a166be14ef23a92938b
Gui: Change font to Fixed in options dialog
src/mentor.py