# HG changeset patch # User wenzelm # Date 856177200 -3600 # Node ID a7f469c0ba592501c9c3f423e7a05fc52604b782 # Parent 3c3a84cc85a90c0e11eb71ad4f1eeba77750d432 tuned comments; diff -r 3c3a84cc85a9 -r a7f469c0ba59 lib/scripts/getsettings --- a/lib/scripts/getsettings Mon Feb 17 11:04:00 1997 +0100 +++ b/lib/scripts/getsettings Mon Feb 17 12:00:00 1997 +0100 @@ -9,7 +9,7 @@ set -o allexport -#users tend to put strange things in here +#users tend to put strange things in here ... unset ENV unset BASH_ENV @@ -18,6 +18,7 @@ unset OSTYPE PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE') +#get actual settings . $ISABELLE_HOME/etc/settings || exit 2 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings