# HG changeset patch
# User wenzelm
# Date 1621361942 -7200
# Node ID b13b2c1d419ef66e699a10667c7a3722c5302d54
# Parent  9b77e267e6a97abdaa85dc10ce4cee639ada404f
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;

diff -r 9b77e267e6a9 -r b13b2c1d419e src/Doc/Tutorial/document/build
--- 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"
diff -r 9b77e267e6a9 -r b13b2c1d419e src/Doc/prepare_document
--- 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
diff -r 9b77e267e6a9 -r b13b2c1d419e src/Pure/Thy/document_build.scala
--- 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"))
       }
     }