lib/Tools/make
changeset 9788 df671fa2562a
parent 7795 111d2a65e1c6
child 10511 efb3428c9879
equal deleted inserted replaced
9787:fb8c5a66dbe8 9788:df671fa2562a
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # DESCRIPTION: Isabelle make utility
     7 # DESCRIPTION: Isabelle make utility
     6 
     8 
     7 
     9 
     8 PRG=$(basename $0)
    10 PRG=$(basename "$0")
     9 
    11 
    10 function usage()
    12 function usage()
    11 {
    13 {
    12   echo
    14   echo
    13   echo "Usage: $PRG [ARGS ...]"
    15   echo "Usage: $PRG [ARGS ...]"