diff -r bae5683c2891 -r 3b1086cf2f4d lib/Tools/getenv
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/getenv	Mon Dec 02 18:19:50 1996 +0100
@@ -0,0 +1,23 @@
+#!/bin/bash
+#
+# DESCRIPTION: get value from Isabelle settings
+#
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG VARNAME"
+  echo
+  echo "  Get value of VARNAME from the Isabelle settings."
+  echo
+  exit 1
+}
+
+
+## main
+
+[ $# -ne 1 ] && usage
+
+eval "echo \$$1"