lib/Tools/env

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/env	Sun Oct 19 20:09:37 2008 +0200
@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Markus Wenzel, TU Muenchen
+#
+# DESCRIPTION: run a program in a modified environment
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [CMDLINE ...]"
+  echo
+  echo
+  echo "  Run CMDLINE within the Isabelle environment (via the system's env command)."
+  echo
+  exit 1
+}
+
+
+## main
+
+[ "$1" = "-?" ] && usage
+
+exec /usr/bin/env "$@"