# HG changeset patch
# User wenzelm
# Date 1224439777 -7200
# Node ID 809dda85079d36c6925e44eb8c2f86e465fe3d31
# Parent  7aabaf1ba263067c08aa973ddc872e3ace89429e
run a program in a modified environment;

diff -r 7aabaf1ba263 -r 809dda85079d 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 "$@"