lib/Tools/make
author wenzelm
Wed Nov 22 21:41:39 2000 +0100 (2000-11-22)
changeset 10511 efb3428c9879
parent 9788 df671fa2562a
child 10555 2323ec838401
permissions -rwxr-xr-x
tuned;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: Isabelle make utility
     8 
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [ARGS ...]"
    16   echo
    17   echo "  Compile the logic in current directory using IsaMakefile."
    18   echo "  ARGS are directly passed to the system make program."
    19   echo
    20   exit 1
    21 }
    22 
    23 
    24 ## main
    25 
    26 [ "$1" = "-?" ] && usage
    27 
    28 exec make -f IsaMakefile "$@"