# HG changeset patch
# User wenzelm
# Date 931452043 -7200
# Node ID ee6640456cbb6a944cf640099fa7d396790bc1dc
# Parent  c7c365b4f6151dd942d87bddc275f2c90f1b5699
-B option;

diff -r c7c365b4f615 -r ee6640456cbb lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Jul 08 18:39:34 1999 +0200
+++ b/lib/Tools/usedir	Thu Jul 08 18:40:43 1999 +0200
@@ -15,10 +15,11 @@
   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 "    -i BOOL      generate theory browsing information,"
   echo "                 i.e. HTML / graph data (default false)"
-  echo "    -P PATH      set path for remote theory browsing information"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo
@@ -42,9 +43,13 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "bi:rs:P:" OPT
+  while getopts "BP:bi:rs:" OPT
   do
     case "$OPT" in
+      B)
+        BUILD=true
+        export THIS_IS_ISABELLE_BUILD=true
+        ;;
       b)
         BUILD=true
         ;;