equal
deleted
inserted
replaced
8 hg parent --template '{date|shortdate}' > tip.tex |
8 hg parent --template '{date|shortdate}' > tip.tex |
9 |
9 |
10 "$ISABELLE_TOOL" version > version.tex |
10 "$ISABELLE_TOOL" version > version.tex |
11 |
11 |
12 "$ISABELLE_TOOL" latex -o "$FORMAT" |
12 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|
13 "$ISABELLE_TOOL" latex -o "$FORMAT" |
13 "$ISABELLE_TOOL" latex -o bbl |
14 "$ISABELLE_TOOL" latex -o bbl |
14 makeindex -o root.stu root.str |
15 makeindex -o root.stu root.str |
15 "$ISABELLE_TOOL" latex -o "$FORMAT" |
16 "$ISABELLE_TOOL" latex -o "$FORMAT" |
16 "$ISABELLE_TOOL" latex -o "$FORMAT" |
17 "$ISABELLE_TOOL" latex -o "$FORMAT" |
|
18 cp root.pdf ../document.pdf |
17 mv root.pdf ../progtutorial.pdf |
19 mv root.pdf ../progtutorial.pdf |
18 |
20 |
19 |
21 |
20 #"$ISABELLE_HOME/doc-src/sedindex" root |
22 #"$ISABELLE_HOME/doc-src/sedindex" root |
21 #+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out |
23 #+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out |