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 }