[plt-scheme] DrScheme/HelpDesk menu fonts

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.

Cheers,
jao
-- 
Outside of a dog, a book is a man's best friend: and inside a dog,
it's too dark to read. - Groucho Marx
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 188 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20070310/7cf939ad/attachment.sig>