getsettings: bash source script to augment current env.

--- /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