| author | wenzelm |
| Thu, 17 Apr 1997 10:30:57 +0200 | |
| changeset 2968 | 8ba30b031f31 |
| parent 2736 | 476adc742599 |
| child 3118 | 24dae6222579 |
| permissions | -rw-r--r-- |
1 #
2 # $Id$
3 #
4 # getsettings - bash source script to augment current env.
5 #
7 #normalize ISABELLE_HOME as passed by caller
8 export ISABELLE_HOME
9 ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
12 set -o allexport
14 #users tend to put strange things in here ...
15 unset ENV
16 unset BASH_ENV
18 #get actual settings
19 . $ISABELLE_HOME/etc/settings || exit 2
20 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
22 #derived values
23 ISABELLE=$ISABELLE_HOME/bin/isabelle
24 ISATOOL=$ISABELLE_HOME/bin/isatool
26 set +o allexport