changeset 72580 | 531a0c44ea3f |
parent 72578 | 3e8395f9093a |
child 72594 | e00089ddf462 |
--- 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) } }