more interrupts;
authorwenzelm
Wed, 17 Nov 2021 15:46:35 +0100
changeset 74814 79fa9f2d02fa
parent 74813 2ad892ac749a
child 74815 cfc15da73a78
more interrupts;
src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Wed Nov 17 15:23:15 2021 +0100
+++ b/src/Pure/Admin/build_doc.scala	Wed Nov 17 15:46:35 2021 +0100
@@ -52,6 +52,7 @@
       {
         case (doc, session) =>
           try {
+            progress.expose_interrupt()
             progress.echo("Documentation " + quote(doc) + " ...")
 
             using(store.open_database_context())(db_context =>