# HG changeset patch
# User wenzelm
# Date 863625310 -7200
# Node ID 537f7281d42cd30f232d95f976da37fdd632011f
# Parent  3270d7bca92389d7c13f8fed46bd372c60297d10
removed -u option;

diff -r 3270d7bca923 -r 537f7281d42c bin/isabelle
--- a/bin/isabelle	Wed May 14 17:41:15 1997 +0200
+++ b/bin/isabelle	Wed May 14 17:55:10 1997 +0200
@@ -26,7 +26,6 @@
   echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
   echo "    -r           open heap file read-only"
-  echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
   echo
   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
   echo "  These are either names to be searched in the Isabelle path, or actual"
@@ -52,7 +51,7 @@
 TERMINATE=""
 READONLY=""
 
-while getopts "e:m:qru" OPT
+while getopts "e:m:qr" OPT
 do
   case "$OPT" in
     e)
@@ -71,9 +70,6 @@
     r)
       READONLY=true
       ;;
-    u)
-      MLTEXT="$MLTEXT exit_use_dir\".\";"
-      ;;
     \?)
       usage
       ;;