# HG changeset patch # User wenzelm # Date 850823514 -3600 # Node ID 853732a26bdd88fb367707bfed795bd16463b5ba # Parent d5efdfad074dd45b3be65670b366fb0859bf4a52 improved error handling; 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