| changeset 2428 | 853732a26bdd |
| parent 2348 | b51e104ecf40 |
| child 2478 | adbd622bb375 |
| 2427:d5efdfad074d | 2428:853732a26bdd |
|---|---|
7 #value set by caller |
7 #value set by caller |
8 export ISABELLE_HOME |
8 export ISABELLE_HOME |
9 |
9 |
10 set -o allexport |
10 set -o allexport |
11 |
11 |
12 . $ISABELLE_HOME/etc/settings |
12 . $ISABELLE_HOME/etc/settings || exit 2 |
13 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
13 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
14 |
14 |
15 set +o allexport |
15 set +o allexport |