ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
authorwenzelm
Thu, 07 Oct 1999 12:25:20 +0200
changeset 7770 0497323c1f0b
parent 7769 700439dc581e
child 7771 cc8e2263be65
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Oct 07 12:20:21 1999 +0200
+++ b/lib/scripts/getsettings	Thu Oct 07 12:25:20 1999 +0200
@@ -4,8 +4,13 @@
 # getsettings - bash source script to augment current env.
 #
 
+if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
+then
+
 set -o allexport
 
+ISABELLE_SETTINGS_PRESENT=true
+
 #normalize ISABELLE_HOME as passed by caller
 ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
 
@@ -32,3 +37,5 @@
 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
 
 set +o allexport
+
+fi