| changeset 2299 | ed9720047d53 |
| child 2307 | 508d2a233dbc |
| 2298:df82271be07b | 2299:ed9720047d53 |
|---|---|
1 # |
|
2 # getsettings - bash source script to augment current env |
|
3 # |
|
4 # $Id$ |
|
5 # |
|
6 |
|
7 #value set by caller |
|
8 export ISABELLE_HOME |
|
9 |
|
10 set -o allexport |
|
11 |
|
12 . $ISABELLE_HOME/etc/settings |
|
13 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
|
14 |
|
15 set +o allexport |