220.127.116.11 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 18.104.22.168