lib/scripts/getsettings
changeset 62413 c6111df4a4f8
parent 62412 ffdc5cf36dc5
child 62414 1abd90afe387
     1.1 --- a/lib/scripts/getsettings	Thu Feb 25 17:49:04 2016 +0100
     1.2 +++ b/lib/scripts/getsettings	Thu Feb 25 18:05:04 2016 +0100
     1.3 @@ -7,12 +7,11 @@
     1.4  if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
     1.5  then
     1.6  
     1.7 -set -o allexport
     1.8 +export ISABELLE_SETTINGS_PRESENT=true
     1.9  
    1.10 -ISABELLE_SETTINGS_PRESENT=true
    1.11 +export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
    1.12 +source "$BASH_ENV"
    1.13  
    1.14 -BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
    1.15 -source "$BASH_ENV"
    1.16  set -o allexport
    1.17  
    1.18  #sane environment defaults (notably on Mac OS X)