diff -r 5de31ddf9c03 -r 7268a5f425f8 doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Tue Jan 16 00:22:43 2001 +0100
+++ b/doc-src/System/basics.tex	Tue Jan 16 00:23:14 2001 +0100
@@ -218,6 +218,7 @@
     -P           startup Proof General interaction mode
     -c           tell ML system to compress output image
     -e MLTEXT    pass MLTEXT to the ML session
+    -f           pass 'Session.finish();' to the ML session
     -m MODE      add print mode for output
     -q           non-interactive session
     -r           open heap file read-only
@@ -272,8 +273,10 @@
 code is provided. Also make sure that the {\ML} commands are terminated
 properly by semicolon.
 
-\medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
-``\texttt{use"ROOT.ML";}'' to the {\ML} session.
+\medskip The \texttt{-u} option is a shortcut for \texttt{-e} passing
+``\texttt{use"ROOT.ML";}'' to the {\ML} session.  The \texttt{-f} option
+passes ``\texttt{Session.finish();}'', which is intended mainly for
+administrative purposes.
 
 \medskip The \texttt{-m} option adds identifiers of print modes to be made
 active for this session. Typically, this is used by some user interface, e.g.\