lib/Tools/fixdots
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