| author | wenzelm | 
| Tue, 14 Mar 2023 17:34:38 +0100 | |
| changeset 77654 | 78913f29fc21 | 
| parent 73604 | 51b291ae3e2d | 
| permissions | -rwxr-xr-x | 
| 28638 | 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 | ||
| 10 | PRG="$(basename "$0")" | |
| 11 | ||
| 12 | function usage() | |
| 13 | {
 | |
| 14 | echo | |
| 28650 | 15 | echo "Usage: isabelle $PRG [CMDLINE ...]" | 
| 28638 | 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 | ||
| 73604 | 28 | /usr/bin/env "$@" |