equal
deleted
inserted
replaced
19 latex "$NAME" |
19 latex "$NAME" |
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_HOME/doc-src/prepare_document" "$FORMAT" |
25 cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . |
|
26 |
25 |
27 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|
28 "$ISABELLE_TOOL" latex -o bbl |
|
29 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|
30 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|
31 "$ISABELLE_HOME/doc-src/sedindex" root |
|
32 [ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out |
|
33 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|
34 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|