lib/Tools/fixdots
changeset 4508 f102cb0140fe
parent 3826 0caedb36900d
child 6082 590f9e3bf4d8
     1.1 --- a/lib/Tools/fixdots	Fri Jan 02 11:59:06 1998 +0100
     1.2 +++ b/lib/Tools/fixdots	Fri Jan 02 13:24:53 1998 +0100
     1.3 @@ -32,10 +32,5 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -PERL=$(type -path perl)
     1.8 -if [ -z $PERL ]; then
     1.9 -  echo "$PRG fatal error: no perl!?"
    1.10 -else
    1.11 -  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    1.12 -    xargs $PERL $ISABELLE_HOME/lib/scripts/fixdots.pl
    1.13 -fi
    1.14 +find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    1.15 +  xargs perl -w $ISABELLE_HOME/lib/scripts/fixdots.pl