src/Pure/Admin/build_doc.scala
changeset 72599 76550282267f
parent 72597 e8d7dc1c229c
child 72652 07edf1952ab1
--- a/src/Pure/Admin/build_doc.scala	Thu Nov 12 16:07:25 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Thu Nov 12 16:27:31 2020 +0100
@@ -50,7 +50,6 @@
     val errs =
       Par_List.map((doc_session: (String, String)) =>
         try {
-          progress.expose_interrupt()
           Present.build_documents(doc_session._2, deps, store, progress = progress)
           None
         }