Dan Stillman 006509b5d2 Closes #382, Make font sizes configurable/changeable ... Configurable in preferences or via hidden pref for more extreme options Also straightened up diplay of UI options in pref pane		2007-02-01 09:15:37 +00:00
..
preferences	Closes #382, Make font sizes configurable/changeable	2007-02-01 09:15:37 +00:00