author | wenzelm |
Sat, 10 Sep 2022 16:12:52 +0200 | |
changeset 76107 | 4dedb6e2dac2 |
parent 73772 | 6b4c47666267 |
permissions | -rwxr-xr-x |
53498 | 1 |
#!/usr/bin/env bash |
48971 | 2 |
|
3 |
set -e |
|
4 |
||
73740
c46ff0efa1ce
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
wenzelm
parents:
73733
diff
changeset
|
5 |
$ISABELLE_LUALATEX root |
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
|
6 |
|
73742 | 7 |
if [ -f manual.bib -o -f root.bib ] |
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 |
then |
73740
c46ff0efa1ce
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
wenzelm
parents:
73733
diff
changeset
|
9 |
$ISABELLE_BIBTEX root |
c46ff0efa1ce
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
wenzelm
parents:
73733
diff
changeset
|
10 |
$ISABELLE_LUALATEX root |
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
|
11 |
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
|
12 |
|
73740
c46ff0efa1ce
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
wenzelm
parents:
73733
diff
changeset
|
13 |
$ISABELLE_LUALATEX root |
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
|
14 |
|
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
|
15 |
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
|
16 |
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
|
17 |
"$ISABELLE_HOME/src/Doc/sedindex" root |
73740
c46ff0efa1ce
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
wenzelm
parents:
73733
diff
changeset
|
18 |
$ISABELLE_LUALATEX root |
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
|
19 |
fi |