[plt-scheme] DrScheme/HelpDesk menu fonts

At Sat, 10 Mar 2007 00:31:08 +0100, "Jose A. Ortega Ruiz" wrote:
> Hi. I'm sure i'm overlooking an obvious answer, but how does one
> change the font used by DrScheme and HelpDesk for their menus?
> Actually, i just want to change their size, but i've been tinkering
> around with the config file in ~/.plt-scheme and MrEd's preferences
> without success.

You should be able to add a line in "~/.plt-scheme/plt-prefs.ss". For
example,

 (|MrEd:controlFontSize| 32)

would change the menu (and button, etc.) font size to 32.

Matthew