diff -r 8cddc62ed170 -r c567f9fd61a2 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Jun 05 11:31:15 2005 +0200
+++ b/lib/scripts/getsettings	Sun Jun 05 11:31:16 2005 +0200
@@ -47,7 +47,8 @@
 
 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
   { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
-[ -f "$ISABELLE_HOME_USER/etc/settings" ] && source "$ISABELLE_HOME_USER/etc/settings"
+[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
+  source "$ISABELLE_HOME_USER/etc/settings" || exit 2
 
 #append ML system identifier to paths
 if [ -z "$ML_PLATFORM" ]; then