# HG changeset patch
# User wenzelm
# Date 861973732 -7200
# Node ID c16029f41ad9e042a25cf85b4cf71523b21c0528
# Parent  db72904b42fb76657261e2a89a5b1056b8441f87
removed -c option;

diff -r db72904b42fb -r c16029f41ad9 bin/isabelle
--- a/bin/isabelle	Fri Apr 25 15:08:25 1997 +0200
+++ b/bin/isabelle	Fri Apr 25 15:08:52 1997 +0200
@@ -22,7 +22,6 @@
   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
   echo
   echo "  Options are:"
-  echo "    -c           force copying of heap file (for Poly/ML)"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
@@ -48,19 +47,14 @@
 
 # options
 
-COPYDB=""
 MLTEXT=""
-COPYDB=""
 MODES=""
 TERMINATE=""
 READONLY=""
 
-while getopts "ce:m:qru" OPT
+while getopts "e:m:qru" OPT
 do
   case "$OPT" in
-    c)
-      COPYDB=true
-      ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
@@ -166,6 +160,6 @@
 
 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
 
-export INFILE OUTFILE COPYDB MLTEXT TERMINATE
+export INFILE OUTFILE MLTEXT TERMINATE
 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
diff -r db72904b42fb -r c16029f41ad9 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Apr 25 15:08:25 1997 +0200
+++ b/lib/Tools/usedir	Fri Apr 25 15:08:52 1997 +0200
@@ -16,7 +16,6 @@
   echo
   echo "  Options are:"
   echo "    -b           build mode (output heap image, use dir \".\")"
-  echo "    -c           force copying of heap file (for Poly/ML)"
   echo "    -g BOOL      generate theory graph data (default false)"
   echo "    -h BOOL      generate theory HTML data (default false)"
   echo "    -s NAME      override session NAME"
@@ -33,7 +32,6 @@
 # options
 
 BUILD=""
-COPYDB=""
 GRAPH=false
 HTML=false
 SESSION=""
@@ -47,9 +45,6 @@
       b)
         BUILD=true
         ;;
-      c)
-        COPYDB="-c"
-        ;;
       g)
         GRAPH="$OPTARG"
         ;;
@@ -90,7 +85,7 @@
     -e "make_html := $HTML;" \
     -e "set_session\"$SESSION\";" \
     -e "exit_use_dir\".\";" \
-    -q $COPYDB $LOGIC $NAME
+    -q $LOGIC $NAME
 else
   exec $ISABELLE \
     -e "make_html := $HTML;" \