lib/scripts/getsettings
changeset 3185 7a6c933d51d0
parent 3118 24dae6222579
child 6413 b2f2770ef8d9
     1.1 --- a/lib/scripts/getsettings	Wed May 14 18:37:03 1997 +0200
     1.2 +++ b/lib/scripts/getsettings	Wed May 14 18:38:15 1997 +0200
     1.3 @@ -4,12 +4,14 @@
     1.4  # getsettings - bash source script to augment current env.
     1.5  #
     1.6  
     1.7 +set -o allexport
     1.8 +
     1.9  #normalize ISABELLE_HOME as passed by caller
    1.10 -export ISABELLE_HOME
    1.11  ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
    1.12  
    1.13 -
    1.14 -set -o allexport
    1.15 +#main executables
    1.16 +ISABELLE=$ISABELLE_HOME/bin/isabelle
    1.17 +ISATOOL=$ISABELLE_HOME/bin/isatool
    1.18  
    1.19  #users tend to put strange things in here ...
    1.20  unset ENV
    1.21 @@ -19,10 +21,6 @@
    1.22  . $ISABELLE_HOME/etc/settings || exit 2
    1.23  [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    1.24  
    1.25 -#derived values
    1.26 -ISABELLE=$ISABELLE_HOME/bin/isabelle
    1.27 -ISATOOL=$ISABELLE_HOME/bin/isatool
    1.28 -
    1.29  #append ML system to paths
    1.30  ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
    1.31  ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)