lib/Tools/make
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788 df671fa2562a
parent 7795 111d2a65e1c6
child 10511 efb3428c9879
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
     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 "$@"