|
From: <no...@so...> - 2002-03-12 05:00:59
|
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 |