# HG changeset patch
# User wenzelm
# Date 849547391 -3600
# Node ID ed9720047d53de7dabfa38ff9742c10d5f6625d7
# Parent  df82271be07b100f806a68ccd7c0d952b7eaa41b
getsettings: bash source script to augment current env.

diff -r df82271be07b -r ed9720047d53 lib/scripts/getsettings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/getsettings	Mon Dec 02 18:23:11 1996 +0100
@@ -0,0 +1,15 @@
+#
+# getsettings - bash source script to augment current env
+#
+# $Id$
+#
+
+#value set by caller
+export ISABELLE_HOME
+
+set -o allexport
+
+. $ISABELLE_HOME/etc/settings
+[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
+
+set +o allexport