lib/Tools/expandshort
changeset 6082 590f9e3bf4d8
parent 4508 f102cb0140fe
child 7498 1e5585fd3632
--- a/lib/Tools/expandshort	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/expandshort	Tue Jan 12 12:17:53 1999 +0100
@@ -32,4 +32,7 @@
 
 ## main
 
-find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/expandshort.pl
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/expandshort.pl