LP, the Larch Prover -- The log-file setting

The log-file setting provides a means of recording the current LP session in a file.


<set-log-file-command> ::= set log-file <file>


set log session


The set log command causes LP to start recording the terminal session in a file named <file>.lplog (unless <file> contains a period, in which case LP does not supply the suffix .lplog) in LP's current working directory. Any previous contents of this log file are lost. If LP was already logging to a file, that file is closed before opening the new log file. Logging is ended by the quit or unset log commands.