more interrupts;
authorwenzelm
Wed, 11 Nov 2020 23:06:27 +0100
changeset 72580 531a0c44ea3f
parent 72579 d9cf3fa0300b
child 72581 de581f98a3a1
more interrupts;
src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Wed Nov 11 22:30:00 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Wed Nov 11 23:06:27 2020 +0100
@@ -50,6 +50,7 @@
       options + "document=pdf" + "document_output=~~/doc" + "document_output_sources=false"
     val deps = Sessions.load_structure(doc_options).selection_deps(selection)
     for (session <- selection.sessions) {
+      progress.expose_interrupt()
       Present.build_documents(session, deps, store, progress = progress)
     }
   }