1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/env	Sun Oct 19 20:09:37 2008 +0200
     1.3 @@ -0,0 +1,29 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +#
     1.9 +# DESCRIPTION: run a program in a modified environment
    1.10 +
    1.11 +
    1.12 +## diagnostics
    1.13 +
    1.14 +PRG="$(basename "$0")"
    1.15 +
    1.16 +function usage()
    1.17 +{
    1.18 +  echo
    1.19 +  echo "Usage: $PRG [CMDLINE ...]"
    1.20 +  echo
    1.21 +  echo
    1.22 +  echo "  Run CMDLINE within the Isabelle environment (via the system's env command)."
    1.23 +  echo
    1.24 +  exit 1
    1.25 +}
    1.26 +
    1.27 +
    1.28 +## main
    1.29 +
    1.30 +[ "$1" = "-?" ] && usage
    1.31 +
    1.32 +exec /usr/bin/env "$@"