added ISABELLE_SITE_SETTINGS_PRESENT;
authorwenzelm
Sat, 01 Jul 2000 19:49:48 +0200
changeset 9227 298ae5f69b18
parent 9226 cbe6144f0f15
child 9228 672b03038110
added ISABELLE_SITE_SETTINGS_PRESENT;
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