diff -r 6715b2ce44d4 -r 72a719e997b9 doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Thu Sep 28 14:47:42 2000 +0200
+++ b/doc-src/System/basics.tex	Thu Sep 28 14:48:05 2000 +0200
@@ -213,6 +213,7 @@
 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
 
   Options are:
+    -C           tell ML system to copy output image
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -c           tell ML system to compress output image
@@ -261,6 +262,10 @@
 garbage collected and all values maximally shared, resulting in up to 50\%
 less disk space consumption.
 
+\medskip The \texttt{-C} option tells the ML system to produce a completely
+self-contained output image, probably including a copy of the ML runtime
+system itself.
+
 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
 the Isabelle session from the command line. Multiple \texttt{-e}'s are
 evaluated in the given order. Strange things may happen when errorneous {\ML}