Feature Requests item #528813, was opened at 2002-03-11 23:00
You can respond by visiting:
http://sourceforge.net/tracker/?func=detail&atid=438938&aid=528813&group_id=44253
Category: User interface
Group: Small (< 1 pair-week)
Status: Open
Priority: 6
Submitted By: Robby Morgan (ricerobs)
Assigned to: Robby Morgan (ricerobs)
Summary: Allow font size manipulation
Initial Comment:
DrJava needs a way to change the default font size
without recompiling the whole program. This will
eventually be part of the larger configuration
project, but it was deemed necessary enough to
implement in the current config framework.
----------------------------------------------------------------------
You can respond by visiting:
http://sourceforge.net/tracker/?func=detail&atid=438938&aid=528813&group_id=44253
|
