| author | wenzelm | 
| Mon, 22 Jun 1998 15:18:02 +0200 | |
| changeset 5062 | fbdb0b541314 | 
| parent 3185 | 7a6c933d51d0 | 
| child 6413 | b2f2770ef8d9 | 
| permissions | -rw-r--r-- | 
| 2307 | 1 | # | 
| 2 | # $Id$ | |
| 2299 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 3 | # | 
| 2348 | 4 | # getsettings - bash source script to augment current env. | 
| 2299 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 5 | # | 
| 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 6 | |
| 3185 | 7 | set -o allexport | 
| 8 | ||
| 2736 | 9 | #normalize ISABELLE_HOME as passed by caller | 
| 10 | ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD) | |
| 11 | ||
| 3185 | 12 | #main executables | 
| 13 | ISABELLE=$ISABELLE_HOME/bin/isabelle | |
| 14 | ISATOOL=$ISABELLE_HOME/bin/isatool | |
| 2299 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 15 | |
| 2643 | 16 | #users tend to put strange things in here ... | 
| 2621 | 17 | unset ENV | 
| 18 | unset BASH_ENV | |
| 19 | ||
| 2643 | 20 | #get actual settings | 
| 2428 | 21 | . $ISABELLE_HOME/etc/settings || exit 2 | 
| 2299 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 22 | [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings | 
| 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 23 | |
| 3118 | 24 | #append ML system to paths | 
| 25 | ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM" | |
| 26 | ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done) | |
| 27 | ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) | |
| 28 | ||
| 2299 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 29 | set +o allexport |