more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
--- a/src/Doc/Tutorial/document/build Tue May 18 19:59:22 2021 +0200
+++ b/src/Doc/Tutorial/document/build Tue May 18 20:19:02 2021 +0200
@@ -7,6 +7,7 @@
isabelle latex -o "$FORMAT"
isabelle latex -o bbl
+isabelle latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
./isa-index root
isabelle latex -o "$FORMAT"
-isabelle latex -o "$FORMAT"
--- a/src/Doc/prepare_document Tue May 18 19:59:22 2021 +0200
+++ b/src/Doc/prepare_document Tue May 18 20:19:02 2021 +0200
@@ -5,7 +5,17 @@
FORMAT="$1"
isabelle latex -o "$FORMAT"
-isabelle latex -o bbl
-[ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
+
+if [ -f root.bib ]
+then
+ isabelle latex -o bbl
+ isabelle latex -o "$FORMAT"
+fi
+
isabelle latex -o "$FORMAT"
-isabelle latex -o "$FORMAT"
+
+if [ -f root.idx ]
+then
+ "$ISABELLE_HOME/src/Doc/sedindex" root
+ isabelle latex -o "$FORMAT"
+fi
--- a/src/Pure/Thy/document_build.scala Tue May 18 19:59:22 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Tue May 18 20:19:02 2021 +0200
@@ -348,14 +348,17 @@
List(
"set -e",
latex_bash(),
- "if [ -f " + root_bash("bib") + " ]; then",
+ "if [ -f " + root_bash("bib") + " ]",
+ "then",
" " + latex_bash("bbl"),
- "fi",
- "if [ -f " + root_bash("idx") + " ]; then",
- " " + latex_bash("idx"),
+ " " + latex_bash(),
"fi",
latex_bash(),
- latex_bash()))
+ "if [ -f " + root_bash("idx") + " ]",
+ "then",
+ " " + latex_bash("idx"),
+ " " + latex_bash(),
+ "fi"))
}
}