equal
deleted
inserted
replaced
1 # |
1 # |
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 #value set by caller |
7 #value set by caller |
8 export ISABELLE_HOME |
8 export ISABELLE_HOME |
9 |
9 |