lib/scripts/getsettings
changeset 2307 508d2a233dbc
parent 2299 ed9720047d53
child 2348 b51e104ecf40
equal deleted inserted replaced
2306:0aadfaf8557a 2307:508d2a233dbc
       
     1 #
       
     2 # $Id$
     1 #
     3 #
     2 # getsettings - bash source script to augment current env
     4 # getsettings - bash source script to augment current env
     3 #
       
     4 # $Id$
       
     5 #
     5 #
     6 
     6 
     7 #value set by caller
     7 #value set by caller
     8 export ISABELLE_HOME
     8 export ISABELLE_HOME
     9 
     9