equal
deleted
inserted
replaced
20 $ISABELLE_DVIPS -E -o "$NAME.eps" "$NAME.dvi" |
20 $ISABELLE_DVIPS -E -o "$NAME.eps" "$NAME.dvi" |
21 $ISABELLE_EPSTOPDF "$NAME.eps" |
21 $ISABELLE_EPSTOPDF "$NAME.eps" |
22 done |
22 done |
23 |
23 |
24 "$ISABELLE_TOOL" latex -o sty |
24 "$ISABELLE_TOOL" latex -o sty |
|
25 cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . |
|
26 |
25 "$ISABELLE_TOOL" latex -o "$FORMAT" |
27 "$ISABELLE_TOOL" latex -o "$FORMAT" |
26 "$ISABELLE_TOOL" latex -o bbl |
28 "$ISABELLE_TOOL" latex -o bbl |
27 "$ISABELLE_TOOL" latex -o "$FORMAT" |
29 "$ISABELLE_TOOL" latex -o "$FORMAT" |
28 "$ISABELLE_TOOL" latex -o "$FORMAT" |
30 "$ISABELLE_TOOL" latex -o "$FORMAT" |
29 "$ISABELLE_HOME/doc-src/sedindex" root |
31 "$ISABELLE_HOME/doc-src/sedindex" root |