| author | mueller | 
| Tue, 09 Sep 1997 11:14:20 +0200 | |
| changeset 3661 | 1ea4a45b9412 | 
| 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  |