# HG changeset patch
# User wenzelm
# Date 939309547 -7200
# Node ID b43b1c4f27ced9ec2d5b30379b8324a31c598444
# Parent  cf9d07ad62afade7e8068a1e840d8b8034f69be8
unset ISABELLE_SETTINGS_PRESENT;

diff -r cf9d07ad62af -r b43b1c4f27ce lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Oct 07 15:40:32 1999 +0200
+++ b/lib/Tools/usedir	Thu Oct 07 17:19:07 1999 +0200
@@ -54,6 +54,7 @@
     case "$OPT" in
       B)
         BUILD=true
+        unset ISABELLE_SETTINGS_PRESENT
         export THIS_IS_ISABELLE_BUILD=true
         ;;
       b)