lib/Tools/make
changeset 9788 df671fa2562a
parent 7795 111d2a65e1c6
child 10511 efb3428c9879
     1.1 --- a/lib/Tools/make	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/make	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,11 +1,13 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # DESCRIPTION: Isabelle make utility
    1.11  
    1.12  
    1.13 -PRG=$(basename $0)
    1.14 +PRG=$(basename "$0")
    1.15  
    1.16  function usage()
    1.17  {