getenv: get value from Isabelle settings.
authorwenzelm
Mon, 02 Dec 1996 18:19:50 +0100
changeset 2296 3b1086cf2f4d
parent 2295 bae5683c2891
child 2297 efcabc6df91a
getenv: get value from Isabelle settings.
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"