changeset 62413 | c6111df4a4f8 |
parent 62412 | ffdc5cf36dc5 |
child 62414 | 1abd90afe387 |
--- a/lib/scripts/getsettings Thu Feb 25 17:49:04 2016 +0100 +++ b/lib/scripts/getsettings Thu Feb 25 18:05:04 2016 +0100 @@ -7,12 +7,11 @@ if [ -z "$ISABELLE_SETTINGS_PRESENT" ] then -set -o allexport +export ISABELLE_SETTINGS_PRESENT=true -ISABELLE_SETTINGS_PRESENT=true +export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions" +source "$BASH_ENV" -BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions" -source "$BASH_ENV" set -o allexport #sane environment defaults (notably on Mac OS X)