equal
deleted
inserted
replaced
15 cp "$ISABELLE_HOME/doc-src/ttbox.sty" . |
15 cp "$ISABELLE_HOME/doc-src/ttbox.sty" . |
16 cp "$ISABELLE_HOME/doc-src/underscore.sty" . |
16 cp "$ISABELLE_HOME/doc-src/underscore.sty" . |
17 cp "$ISABELLE_HOME/doc-src/manual.bib" . |
17 cp "$ISABELLE_HOME/doc-src/manual.bib" . |
18 |
18 |
19 "$ISABELLE_TOOL" latex -o sty |
19 "$ISABELLE_TOOL" latex -o sty |
|
20 cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . |
|
21 |
20 "$ISABELLE_TOOL" latex -o "$FORMAT" |
22 "$ISABELLE_TOOL" latex -o "$FORMAT" |
21 "$ISABELLE_TOOL" latex -o bbl |
23 "$ISABELLE_TOOL" latex -o bbl |
22 "$ISABELLE_TOOL" latex -o "$FORMAT" |
24 "$ISABELLE_TOOL" latex -o "$FORMAT" |
23 "$ISABELLE_TOOL" latex -o "$FORMAT" |
25 "$ISABELLE_TOOL" latex -o "$FORMAT" |
24 "$ISABELLE_HOME/doc-src/sedindex" root |
26 "$ISABELLE_HOME/doc-src/sedindex" root |