changeset 9788 | df671fa2562a |
parent 7795 | 111d2a65e1c6 |
child 10511 | efb3428c9879 |
--- a/lib/Tools/make Fri Sep 01 17:48:31 2000 +0200 +++ b/lib/Tools/make Fri Sep 01 17:50:36 2000 +0200 @@ -1,11 +1,13 @@ #!/bin/bash # # $Id$ +# Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) # # DESCRIPTION: Isabelle make utility -PRG=$(basename $0) +PRG=$(basename "$0") function usage() {