# HG changeset patch
# User wenzelm
# Date 1605132387 -3600
# Node ID 531a0c44ea3f397eb65c525dfdcfb10e41922d13
# Parent  d9cf3fa0300b4377a3fe6ee8301a43c7e6b433e6
more interrupts;

diff -r d9cf3fa0300b -r 531a0c44ea3f 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)
     }
   }