lib/Tools/fixdots
changeset 9788 df671fa2562a
parent 6082 590f9e3bf4d8
child 10511 efb3428c9879
     1.1 --- a/lib/Tools/fixdots	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/fixdots	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,13 +1,15 @@
     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: ensure that dots in formulas are followed by non-idents
    1.11  
    1.12  
    1.13  ## diagnostics
    1.14  
    1.15 -PRG=$(basename $0)
    1.16 +PRG=$(basename "$0")
    1.17  
    1.18  function usage()
    1.19  {
    1.20 @@ -25,9 +27,9 @@
    1.21  
    1.22  ## process command line
    1.23  
    1.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
    1.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    1.26  
    1.27 -SPECS="$@"; shift $#
    1.28 +SPECS="$@"; shift "$#"
    1.29  
    1.30  
    1.31  ## main
    1.32 @@ -36,4 +38,4 @@
    1.33  AUTO_PERL=perl
    1.34  
    1.35  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    1.36 -  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdots.pl
    1.37 +  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdots.pl"