more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
authorwenzelm
Tue, 18 May 2021 20:19:02 +0200
changeset 73989 b13b2c1d419e
parent 73988 9b77e267e6a9
child 73990 f7f0d516df0c
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
src/Doc/Tutorial/document/build
src/Doc/prepare_document
src/Pure/Thy/document_build.scala
--- 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"))
       }
     }