COMMAND-FILE : FLAG
COMMAND-FILE is a flag or parameter.
The file recording commands.
COMMAND-FILE takes values of type FILESPEC.
It belongs to subjects EVENTS .
Its default value is "/home/theorem/tps/etps3.command"
Its current value is "/home/theorem/tps/etps3.command".
TPS documentation homepage