observe ISABELLE_IGNORE_USER_SETTINGS;
authorwenzelm
Sun Jun 05 11:31:16 2005 +0200 (2005-06-05)
changeset 16253c567f9fd61a2
parent 16252 8cddc62ed170
child 16254 1b2683e18fd2
observe ISABELLE_IGNORE_USER_SETTINGS;
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Sun Jun 05 11:31:15 2005 +0200
     1.2 +++ b/lib/scripts/getsettings	Sun Jun 05 11:31:16 2005 +0200
     1.3 @@ -47,7 +47,8 @@
     1.4  
     1.5  [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
     1.6    { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
     1.7 -[ -f "$ISABELLE_HOME_USER/etc/settings" ] && source "$ISABELLE_HOME_USER/etc/settings"
     1.8 +[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
     1.9 +  source "$ISABELLE_HOME_USER/etc/settings" || exit 2
    1.10  
    1.11  #append ML system identifier to paths
    1.12  if [ -z "$ML_PLATFORM" ]; then