author | wenzelm |
Tue, 18 May 2021 20:19:02 +0200 | |
changeset 73733 | b13b2c1d419e |
parent 73731 | a1ef2589c33f |
child 73740 | c46ff0efa1ce |
permissions | -rwxr-xr-x |
53498 | 1 |
#!/usr/bin/env bash |
48971 | 2 |
|
3 |
set -e |
|
4 |
||
5 |
FORMAT="$1" |
|
6 |
||
62589
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents:
53498
diff
changeset
|
7 |
isabelle latex -o "$FORMAT" |
73733
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
8 |
|
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
9 |
if [ -f root.bib ] |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
10 |
then |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
11 |
isabelle latex -o bbl |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
12 |
isabelle latex -o "$FORMAT" |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
13 |
fi |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
14 |
|
62589
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents:
53498
diff
changeset
|
15 |
isabelle latex -o "$FORMAT" |
73733
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
16 |
|
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
17 |
if [ -f root.idx ] |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
18 |
then |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
19 |
"$ISABELLE_HOME/src/Doc/sedindex" root |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
20 |
isabelle latex -o "$FORMAT" |
b13b2c1d419e
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
wenzelm
parents:
73731
diff
changeset
|
21 |
fi |