[DrJava] [ drjava-Feature Requests-528813 ] Allow font size manipulation

[<no...@so...>]

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