# HG changeset patch # User wenzelm # Date 939299480 -7200 # Node ID d4a6464ed61e61b7af48999606c4a312354d6d7b # Parent 7a8e91b8c100a6488b5228924555c3ad0f6ba5c7 unset ISABELLE_SETTINGS_PRESENT; diff -r 7a8e91b8c100 -r d4a6464ed61e build --- a/build Thu Oct 07 14:31:01 1999 +0200 +++ b/build Thu Oct 07 14:31:20 1999 +0200 @@ -160,6 +160,7 @@ HOST=$(hostname) echo "Started at $DATE ($HOST)" +unset ISABELLE_SETTINGS_PRESENT export THIS_IS_ISABELLE_BUILD=true for L in $MAKE_LOGICS