lib/scripts/getsettings
author wenzelm
Wed May 14 18:38:15 1997 +0200 (1997-05-14)
changeset 3185 7a6c933d51d0
parent 3118 24dae6222579
child 6413 b2f2770ef8d9
permissions -rw-r--r--
tuned;
     1 #
     2 # $Id$
     3 #
     4 # getsettings - bash source script to augment current env.
     5 #
     6 
     7 set -o allexport
     8 
     9 #normalize ISABELLE_HOME as passed by caller
    10 ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
    11 
    12 #main executables
    13 ISABELLE=$ISABELLE_HOME/bin/isabelle
    14 ISATOOL=$ISABELLE_HOME/bin/isatool
    15 
    16 #users tend to put strange things in here ...
    17 unset ENV
    18 unset BASH_ENV
    19 
    20 #get actual settings
    21 . $ISABELLE_HOME/etc/settings || exit 2
    22 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    23 
    24 #append ML system to paths
    25 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
    26 ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)
    27 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
    28 
    29 set +o allexport