[DrJava] [ drjava-Feature Requests-567575 ] GUI Preferences dialog

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

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