1#!/usr/bin/env bash
2#
3# Author: Markus Wenzel, TU Muenchen
4#
5# DESCRIPTION: run a program in a modified environment
6
7
8## diagnostics
9
10PRG="$(basename "$0")"
11
12function usage()
13{
14  echo
15  echo "Usage: isabelle $PRG [CMDLINE ...]"
16  echo
17  echo
18  echo "  Run CMDLINE within the Isabelle environment (via the system's env command)."
19  echo
20  exit 1
21}
22
23
24## main
25
26[ "$1" = "-?" ] && usage
27
28exec /usr/bin/env "$@"
29