equal
deleted
inserted
replaced
3 set -e |
3 set -e |
4 |
4 |
5 FORMAT="$1" |
5 FORMAT="$1" |
6 |
6 |
7 isabelle latex -o "$FORMAT" |
7 isabelle latex -o "$FORMAT" |
8 isabelle latex -o bbl |
8 |
9 [ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root |
9 if [ -f root.bib ] |
|
10 then |
|
11 isabelle latex -o bbl |
|
12 isabelle latex -o "$FORMAT" |
|
13 fi |
|
14 |
10 isabelle latex -o "$FORMAT" |
15 isabelle latex -o "$FORMAT" |
11 isabelle latex -o "$FORMAT" |
16 |
|
17 if [ -f root.idx ] |
|
18 then |
|
19 "$ISABELLE_HOME/src/Doc/sedindex" root |
|
20 isabelle latex -o "$FORMAT" |
|
21 fi |