lib/Tools/logo
changeset 6082 590f9e3bf4d8
parent 5587 7fceb6eea475
child 9788 df671fa2562a
     1.1 --- a/lib/Tools/logo	Mon Jan 11 18:45:46 1999 +0100
     1.2 +++ b/lib/Tools/logo	Tue Jan 12 12:17:53 1999 +0100
     1.3 @@ -69,9 +69,12 @@
     1.4    OUTFILE="isabelle${OUTFILE}.eps"
     1.5  fi
     1.6  
     1.7 +#set by configure
     1.8 +AUTO_PERL=perl
     1.9 +
    1.10  if [ "$OUTFILE" = "-" ]; then
    1.11 -  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    1.12 +  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    1.13  else
    1.14    [ -z "$QUIET" ] && echo "$OUTFILE" >&2
    1.15 -  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
    1.16 +  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
    1.17  fi