lib/Tools/env
author blanchet
Thu Sep 04 11:20:59 2014 +0200 (2014-09-04)
changeset 58182 82478e6c60cb
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
tweaked setup for datatype realizer
     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
    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 
    28 exec /usr/bin/env "$@"