author | wenzelm |
Wed, 11 Nov 2020 23:06:27 +0100 | |
changeset 72580 | 531a0c44ea3f |
parent 72579 | d9cf3fa0300b |
child 72581 | de581f98a3a1 |
--- 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) } }