diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/logo
--- a/lib/Tools/logo	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/logo	Tue Jan 12 12:17:53 1999 +0100
@@ -69,9 +69,12 @@
   OUTFILE="isabelle${OUTFILE}.eps"
 fi
 
+#set by configure
+AUTO_PERL=perl
+
 if [ "$OUTFILE" = "-" ]; then
-  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
+  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
 else
   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
-  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
+  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
 fi