lib/Tools/env
author paulson
Tue, 02 Feb 2010 09:48:20 +0000
changeset 35503 7bba12c3b7b6
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
Correction of a tiny error
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28638
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     2
#
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     4
#
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: run a program in a modified environment
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     6
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     7
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     8
## diagnostics
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
     9
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    11
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    12
function usage()
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    13
{
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    14
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28638
diff changeset
    15
  echo "Usage: isabelle $PRG [CMDLINE ...]"
28638
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    16
  echo
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    17
  echo
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    18
  echo "  Run CMDLINE within the Isabelle environment (via the system's env command)."
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    19
  echo
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    20
  exit 1
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    21
}
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    22
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    23
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    24
## main
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    25
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    26
[ "$1" = "-?" ] && usage
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    27
809dda85079d run a program in a modified environment;
wenzelm
parents:
diff changeset
    28
exec /usr/bin/env "$@"