lib/scripts/getsettings
changeset 2299 ed9720047d53
child 2307 508d2a233dbc
equal deleted inserted replaced
2298:df82271be07b 2299:ed9720047d53
       
     1 #
       
     2 # getsettings - bash source script to augment current env
       
     3 #
       
     4 # $Id$
       
     5 #
       
     6 
       
     7 #value set by caller
       
     8 export ISABELLE_HOME
       
     9 
       
    10 set -o allexport
       
    11 
       
    12 . $ISABELLE_HOME/etc/settings
       
    13 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
       
    14 
       
    15 set +o allexport