author | wenzelm |
Tue, 07 Jan 1997 09:06:01 +0100 | |
changeset 2478 | adbd622bb375 |
parent 2428 | 853732a26bdd |
child 2590 | 363b2c37a1b9 |
permissions | -rw-r--r-- |
# # $Id$ # # getsettings - bash source script to augment current env. # #value set by caller export ISABELLE_HOME set -o allexport . $ISABELLE_HOME/etc/settings || exit 2 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings ISABELLE=$ISABELLE_HOME/bin/isabelle ISATOOL=$ISABELLE_HOME/bin/isatool set +o allexport