| changeset 73723 | 1bbbaae6b5e3 |
| parent 62589 | b5783412bfed |
| child 73731 | a1ef2589c33f |
| 73722:9e1de6fb9579 | 73723:1bbbaae6b5e3 |
|---|---|
3 set -e |
3 set -e |
4 |
4 |
5 FORMAT="$1" |
5 FORMAT="$1" |
6 VARIANT="$2" |
6 VARIANT="$2" |
7 |
7 |
8 isabelle logo HOL |
|
9 isabelle latex -o "$FORMAT" |
8 isabelle latex -o "$FORMAT" |
10 isabelle latex -o bbl |
9 isabelle latex -o bbl |
11 ./isa-index root |
10 ./isa-index root |
12 isabelle latex -o "$FORMAT" |
11 isabelle latex -o "$FORMAT" |
13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out |
12 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out |