lib/Tools/logo
changeset 6082 590f9e3bf4d8
parent 5587 7fceb6eea475
child 9788 df671fa2562a
equal deleted inserted replaced
6081:aa97eb904692 6082:590f9e3bf4d8
    67   OUTFILE=$(echo "$NAME" | tr A-Z a-z)
    67   OUTFILE=$(echo "$NAME" | tr A-Z a-z)
    68   [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
    68   [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
    69   OUTFILE="isabelle${OUTFILE}.eps"
    69   OUTFILE="isabelle${OUTFILE}.eps"
    70 fi
    70 fi
    71 
    71 
       
    72 #set by configure
       
    73 AUTO_PERL=perl
       
    74 
    72 if [ "$OUTFILE" = "-" ]; then
    75 if [ "$OUTFILE" = "-" ]; then
    73   perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    76   $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    74 else
    77 else
    75   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
    78   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
    76   perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
    79   $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
    77 fi
    80 fi