lib/scripts/getsettings
changeset 2643 a7f469c0ba59
parent 2621 e9e491033b54
child 2736 476adc742599
equal deleted inserted replaced
2642:3c3a84cc85a9 2643:a7f469c0ba59
     7 #value set by caller
     7 #value set by caller
     8 export ISABELLE_HOME
     8 export ISABELLE_HOME
     9 
     9 
    10 set -o allexport
    10 set -o allexport
    11 
    11 
    12 #users tend to put strange things in here
    12 #users tend to put strange things in here ...
    13 unset ENV
    13 unset ENV
    14 unset BASH_ENV
    14 unset BASH_ENV
    15 
    15 
    16 #get bash-style platform info -- has to work around some tricky features
    16 #get bash-style platform info -- has to work around some tricky features
    17 unset HOSTTYPE
    17 unset HOSTTYPE
    18 unset OSTYPE
    18 unset OSTYPE
    19 PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
    19 PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
    20 
    20 
       
    21 #get actual settings
    21 . $ISABELLE_HOME/etc/settings || exit 2
    22 . $ISABELLE_HOME/etc/settings || exit 2
    22 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    23 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    23 
    24 
    24 ISABELLE=$ISABELLE_HOME/bin/isabelle
    25 ISABELLE=$ISABELLE_HOME/bin/isabelle
    25 ISATOOL=$ISABELLE_HOME/bin/isatool
    26 ISATOOL=$ISABELLE_HOME/bin/isatool