diff -r 700439dc581e -r 0497323c1f0b lib/scripts/getsettings --- a/lib/scripts/getsettings Thu Oct 07 12:20:21 1999 +0200 +++ b/lib/scripts/getsettings Thu Oct 07 12:25:20 1999 +0200 @@ -4,8 +4,13 @@ # getsettings - bash source script to augment current env. # +if [ -z "$ISABELLE_SETTINGS_PRESENT" ] +then + set -o allexport +ISABELLE_SETTINGS_PRESENT=true + #normalize ISABELLE_HOME as passed by caller ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD) @@ -32,3 +37,5 @@ ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) set +o allexport + +fi