unset ISABELLE_SETTINGS_PRESENT;
authorwenzelm
Thu, 07 Oct 1999 17:19:07 +0200
changeset 7787 b43b1c4f27ce
parent 7786 cf9d07ad62af
child 7788 825b8b1ad136
unset ISABELLE_SETTINGS_PRESENT;
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)