# HG changeset patch
# User wenzelm
# Date 962473788 -7200
# Node ID 298ae5f69b18dd8f0a2300da4a5dcaad33076f8d
# Parent  cbe6144f0f15365e56587086c11ae1c62c3ce8db
added ISABELLE_SITE_SETTINGS_PRESENT;

diff -r cbe6144f0f15 -r 298ae5f69b18 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat Jul 01 19:49:20 2000 +0200
+++ b/lib/scripts/getsettings	Sat Jul 01 19:49:48 2000 +0200
@@ -24,6 +24,7 @@
 
 #get actual settings
 . $ISABELLE_HOME/etc/settings || exit 2
+ISABELLE_SITE_SETTINGS_PRESENT=true
 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
 
 #append ML system identifier to paths