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