22.214.171.124 Saving Options
You can save the current option settings by setting `Edit => Save
Options'. Options are saved in a file named `.ddd/init' in your home
directory when DDD exits. If a session SESSION is active, options will
be saved in `~/.ddd/sessions/SESSION/init' instead.
The options are automatically saved when exiting DDD. You can turn
off this feature by unsetting `Edit => Save Options'. This is tied to
the following resource:
-- Resource: saveOptionsOnExit (class SaveOnExit)
If `on' (default), the current option settings are automatically
saved when DDD exits.
automatically generated by info2www version 126.96.36.199