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