# HG changeset patch
# User wenzelm
# Date 884001382 -3600
# Node ID f90b2d459a1b6449aa33ec7fb3f193d3293ea731
# Parent  44af72721564bdc3724ab397313b1038a3424e0d
added -u option (again);

diff -r 44af72721564 -r f90b2d459a1b bin/isabelle
--- a/bin/isabelle	Mon Jan 05 10:47:10 1998 +0100
+++ b/bin/isabelle	Mon Jan 05 12:56:22 1998 +0100
@@ -26,6 +26,7 @@
   echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
   echo "    -r           open heap file read-only"
+  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
   echo "    -w           reset write permissions on OUTPUT"
   echo
   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
@@ -53,7 +54,7 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "e:m:qrw" OPT
+while getopts "e:m:qruw" OPT
 do
   case "$OPT" in
     e)
@@ -72,6 +73,9 @@
     r)
       READONLY=true
       ;;
+    u)
+      MLTEXT="$MLTEXT use\"ROOT.ML\";"
+      ;;
     w)
       NOWRITE=true
       ;;