lib/Tools/make
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 10555 2323ec838401
child 28650 a7ba12e0d3b7
permissions -rwxr-xr-x
Merged in license change from Isabelle2004
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 #
     6 # DESCRIPTION: Isabelle make utility
     7 
     8 
     9 PRG="$(basename "$0")"
    10 
    11 function usage()
    12 {
    13   echo
    14   echo "Usage: $PRG [ARGS ...]"
    15   echo
    16   echo "  Compile the logic in current directory using IsaMakefile."
    17   echo "  ARGS are directly passed to the system make program."
    18   echo
    19   exit 1
    20 }
    21 
    22 
    23 ## main
    24 
    25 [ "$1" = "-?" ] && usage
    26 
    27 exec make -f IsaMakefile "$@"