# HG changeset patch
# User wenzelm
# Date 940410407 -7200
# Node ID 6e9669c311ae85ea800a619c54ad1c617b7a37a5
# Parent  eedfff88ee40b1c328904546fe39f6d635ade343
removed -B option;

diff -r eedfff88ee40 -r 6e9669c311ae lib/Tools/usedir
--- a/lib/Tools/usedir	Wed Oct 20 11:05:38 1999 +0200
+++ b/lib/Tools/usedir	Wed Oct 20 11:06:47 1999 +0200
@@ -15,7 +15,6 @@
   echo "Usage: $PRG LOGIC NAME"
   echo
   echo "  Options are:"
-  echo "    -B           build mode with THIS_IS_ISABELLE_BUILD indication"
   echo "    -P PATH      set path for remote theory browsing information"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
@@ -47,14 +46,9 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "BP:bc:d:i:rs:" OPT
+  while getopts "P:bc:d:i:rs:" OPT
   do
     case "$OPT" in
-      B)
-        BUILD=true
-        unset ISABELLE_SETTINGS_PRESENT
-        export THIS_IS_ISABELLE_BUILD=true
-        ;;
       b)
         BUILD=true
         ;;