# HG changeset patch
# User wenzelm
# Date 979600994 -3600
# Node ID 7268a5f425f844a723f487061eabede561d1480f
# Parent  5de31ddf9c031a4294aeecf9d1302e9c83a33169
isabelle -f;

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.\ 
diff -r 5de31ddf9c03 -r 7268a5f425f8 src/Pure/mk
--- a/src/Pure/mk	Tue Jan 16 00:22:43 2001 +0100
+++ b/src/Pure/mk	Tue Jan 16 00:23:14 2001 +0100
@@ -93,7 +93,7 @@
   "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-    -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
+    -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   RC="$?"
 else
   ITEM="RAW"
@@ -102,7 +102,7 @@
 
   "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
-    -e "use\"$COMPAT\" handle _ => exit 1;;" \
+    -e "use\"$COMPAT\" handle _ => exit 1;" \
     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   RC="$?"
 fi