equal
deleted
inserted
replaced
3 set -e |
3 set -e |
4 |
4 |
5 FORMAT="$1" |
5 FORMAT="$1" |
6 VARIANT="$2" |
6 VARIANT="$2" |
7 |
7 |
8 "$ISABELLE_TOOL" logo HOL |
8 isabelle logo HOL |
9 "$ISABELLE_TOOL" latex -o "$FORMAT" |
9 isabelle latex -o "$FORMAT" |
10 "$ISABELLE_TOOL" latex -o bbl |
10 isabelle latex -o bbl |
11 ./isa-index root |
11 ./isa-index root |
12 "$ISABELLE_TOOL" latex -o "$FORMAT" |
12 isabelle latex -o "$FORMAT" |
13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out |
13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out |
14 "$ISABELLE_TOOL" latex -o "$FORMAT" |
14 isabelle latex -o "$FORMAT" |