| changeset 6082 | 590f9e3bf4d8 |
| parent 4508 | f102cb0140fe |
| child 9788 | df671fa2562a |
--- a/lib/Tools/nonascii Mon Jan 11 18:45:46 1999 +0100 +++ b/lib/Tools/nonascii Tue Jan 12 12:17:53 1999 +0100 @@ -29,6 +29,9 @@ ## main +#set by configure +AUTO_PERL=perl + find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \ - xargs perl -w -e \ + xargs $AUTO_PERL -w -e \ 'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'