| changeset 2428 | 853732a26bdd |
| parent 2348 | b51e104ecf40 |
| child 2478 | adbd622bb375 |
--- 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