src/Pure/Admin/build_doc.scala
changeset 72580 531a0c44ea3f
parent 72578 3e8395f9093a
child 72594 e00089ddf462
--- 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)
     }
   }