more robust: allow \printindex within the document;
authorwenzelm
Wed, 19 May 2021 11:18:38 +0200
changeset 73994 d701bd96e323
parent 73993 6638323d2774
child 73995 3e44f8c3f059
more robust: allow \printindex within the document;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed May 19 11:15:13 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Wed May 19 11:18:38 2021 +0200
@@ -377,6 +377,7 @@
         "set -e\n" +
         latex_script(context, directory) +
         bibtex_script(context, directory, latex = true) +
+        makeindex_script(context, directory) +
         latex_script(context, directory) +
         makeindex_script(context, directory, latex = true)
       }