equal
deleted
inserted
replaced
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 |
73 #set by configure |
74 AUTO_PERL=perl |
74 AUTO_PERL=/usr/bin/perl |
75 |
75 |
76 if [ "$OUTFILE" = "-" ]; then |
76 if [ "$OUTFILE" = "-" ]; then |
77 "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" |
77 "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" |
78 else |
78 else |
79 [ -z "$QUIET" ] && echo "$OUTFILE" >&2 |
79 [ -z "$QUIET" ] && echo "$OUTFILE" >&2 |