diff -r d5efdfad074d -r 853732a26bdd lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Dec 17 12:51:02 1996 +0100
+++ b/lib/scripts/getsettings	Tue Dec 17 12:51:54 1996 +0100
@@ -9,7 +9,7 @@
 
 set -o allexport
 
-. $ISABELLE_HOME/etc/settings
+. $ISABELLE_HOME/etc/settings || exit 2
 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
 
 set +o allexport