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