diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/nonascii
--- 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: $_"; }}'