equal
deleted
inserted
replaced
2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # getsettings - bash source script to augment current env. |
4 # getsettings - bash source script to augment current env. |
5 # |
5 # |
6 |
6 |
|
7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ] |
|
8 then |
|
9 |
7 set -o allexport |
10 set -o allexport |
|
11 |
|
12 ISABELLE_SETTINGS_PRESENT=true |
8 |
13 |
9 #normalize ISABELLE_HOME as passed by caller |
14 #normalize ISABELLE_HOME as passed by caller |
10 ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD) |
15 ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD) |
11 |
16 |
12 #main executables |
17 #main executables |
30 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
35 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
31 ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done) |
36 ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done) |
32 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) |
37 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) |
33 |
38 |
34 set +o allexport |
39 set +o allexport |
|
40 |
|
41 fi |