All configured options are stored in the .drjava file in the user's home directory. (The location of this file varies on different platforms.) This file is a standard Java properties file, with one option on each line and with option keys and values separated by an equals sign. Any options not defined in this file will have their default value. While it is recommended to use the Preferences window in most cases, the config file can also be edited manually to adjust values as desired. The correct option keys and default values for each option are given in the Available Options section.
Note: All parameters are parsed as standard Java strings, so escape characters must be considered. Notably, to include a Windows-style path in a parameter value, all backslashes must be escaped. For example:
javac.location=c:\\jdk1.4\\lib\\tools.jar |