equal
deleted
inserted
replaced
68 OUTFILE=$(echo "$NAME" | tr A-Z a-z) |
68 OUTFILE=$(echo "$NAME" | tr A-Z a-z) |
69 [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE" |
69 [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE" |
70 OUTFILE="isabelle${OUTFILE}.eps" |
70 OUTFILE="isabelle${OUTFILE}.eps" |
71 fi |
71 fi |
72 |
72 |
73 #set by configure |
|
74 AUTO_PERL=perl |
|
75 |
|
76 if [ "$OUTFILE" = "-" ]; then |
73 if [ "$OUTFILE" = "-" ]; then |
77 "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" |
74 perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" |
78 else |
75 else |
79 [ -z "$QUIET" ] && echo "$OUTFILE" >&2 |
76 [ -z "$QUIET" ] && echo "$OUTFILE" >&2 |
80 "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE" |
77 perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE" |
81 fi |
78 fi |