# HG changeset patch
# User wenzelm
# Date 1243776439 -7200
# Node ID 3c7b40548a84f16ba6490e306948d94763f08da7
# Parent  b58d6a33b57fee8fba4a531a503afa5b7a75d13b
removed obsolete COPYDB flag;

diff -r b58d6a33b57f -r 3c7b40548a84 bin/isabelle-process
--- a/bin/isabelle-process	Sun May 31 15:07:03 2009 +0200
+++ b/bin/isabelle-process	Sun May 31 15:27:19 2009 +0200
@@ -26,7 +26,6 @@
   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
   echo
   echo "  Options are:"
-  echo "    -C           tell ML system to copy output image"
   echo "    -I           startup Isar interaction mode"
   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
@@ -60,7 +59,6 @@
 
 # options
 
-COPYDB=""
 ISAR=false
 PROOFGENERAL=""
 SECURE=""
@@ -73,12 +71,9 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "CIPSW:Xce:fm:qruw" OPT
+while getopts "IPSW:Xce:fm:qruw" OPT
 do
   case "$OPT" in
-    C)
-      COPYDB=true
-      ;;
     I)
       ISAR=true
       ;;
@@ -235,8 +230,7 @@
   NICE=""
 fi
 
-export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
-  ISABELLE_PID ISABELLE_TMP
+export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
diff -r b58d6a33b57f -r 3c7b40548a84 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Sun May 31 15:07:03 2009 +0200
+++ b/doc-src/System/Thy/Basics.thy	Sun May 31 15:27:19 2009 +0200
@@ -266,7 +266,6 @@
 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
 
   Options are:
-    -C           tell ML system to copy output image
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
@@ -326,10 +325,6 @@
   maximally shared, resulting in up to @{text "50%"} less disk space
   consumption.
 
-  \medskip The @{verbatim "-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 @{verbatim "-e"} option, arbitrary ML code may be
   passed to the Isabelle session from the command line. Multiple
   @{verbatim "-e"}'s are evaluated in the given order. Strange things
diff -r b58d6a33b57f -r 3c7b40548a84 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Sun May 31 15:07:03 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Sun May 31 15:27:19 2009 +0200
@@ -275,7 +275,6 @@
 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
 
   Options are:
-    -C           tell ML system to copy output image
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
@@ -337,10 +336,6 @@
   maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
   consumption.
 
-  \medskip The \verb|-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 \verb|-e| option, arbitrary ML code may be
   passed to the Isabelle session from the command line. Multiple
   \verb|-e|'s are evaluated in the given order. Strange things
diff -r b58d6a33b57f -r 3c7b40548a84 lib/scripts/run-mosml
--- a/lib/scripts/run-mosml	Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-mosml	Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
 #
 # Moscow ML 2.00 startup script
 
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
diff -r b58d6a33b57f -r 3c7b40548a84 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-polyml	Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
 #
 # Poly/ML 5.1/5.2 startup script.
 
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
diff -r b58d6a33b57f -r 3c7b40548a84 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-polyml-5.0	Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
 #
 # Poly/ML 5.0 startup script.
 
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
diff -r b58d6a33b57f -r 3c7b40548a84 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-smlnj	Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 110 or later).
 
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics