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