Feature Requests item #567575, was opened at 2002-06-11 19:54
You can respond by visiting:
http://sourceforge.net/tracker/?func=detail&atid=438938&aid=567575&group_id=44253
Category: User interface
Group: Small (< 1 pair-week)
Status: Open
Priority: 6
Submitted By: Charles Reis (csreis)
Assigned to: Nobody/Anonymous (nobody)
Summary: GUI Preferences dialog
Initial Comment:
There should be a "Preferences" item in the Edit menu
which allows editing the config values on the file.
This would (perhaps optionally) write the changes out
to the ".drjava" file in the user's home directory.
This will require making config options updatable on
the fly.
----------------------------------------------------------------------
You can respond by visiting:
http://sourceforge.net/tracker/?func=detail&atid=438938&aid=567575&group_id=44253
|
