# HG changeset patch
# User wenzelm
# Date 1621415918 -7200
# Node ID d701bd96e323e367d6cfb6233caf0e088011a310
# Parent  6638323d2774e578d776c951c57e429cc1d8a964
more robust: allow \printindex within the document;

diff -r 6638323d2774 -r d701bd96e323 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)
       }