| changeset 9227 | 298ae5f69b18 |
| parent 7770 | 0497323c1f0b |
| child 9680 | 6581bfc8421e |
--- 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