more robust: allow \printindex within the document;

--- 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)
       }