--- a/lib/Tools/nonascii Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/nonascii Fri Jan 02 13:24:53 1998 +0100
@@ -29,11 +29,6 @@
## main
-PERL=$(type -path perl)
-if [ -z $PERL ]; then
- echo "$PRG fatal error: no perl!?"
-else
- find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
- xargs $PERL -e \
- 'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
-fi
+find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
+ xargs perl -w -e \
+ 'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'