+++ /dev/null
-<qu>
-option "history_file" -
-#~~~~~~~~~~~~~~~~~~~~~~
-"(default='</qu>DEFAULT_HISTORY_FILE<qu>')"
-string typestr = "filename"
-optional
-details = "
- If </qu>CURRENT_PROGRAM<qu> runs in interactive mode, it reads the history
- file on startup. Upon exit, the in-memory history is appended
- to the history file.
-"
-</qu>