# HG changeset patch # User wenzelm # Date 1605977874 -3600 # Node ID 86fac52c2795c098e7d2122815d65cec628e8e6b # Parent 1cbf36ac4d0b4e5316eac0f7ac8936a7460466b6 more interrupts; diff -r 1cbf36ac4d0b -r 86fac52c2795 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Nov 21 17:30:44 2020 +0100 +++ b/src/Pure/Tools/build.scala Sat Nov 21 17:57:54 2020 +0100 @@ -490,7 +490,7 @@ /* PDF/HTML presentation */ - if (!no_build) { + if (!no_build && !progress.stopped && results.ok) { val presentation_chapters = (for { session_name <- deps.sessions_structure.build_topological_order.iterator @@ -503,6 +503,7 @@ progress.echo("Presentation in " + presentation_dir.absolute) for ((_, (session_name, _)) <- presentation_chapters) { + progress.expose_interrupt() progress.echo("Presenting " + session_name + " ...") Presentation.session_html(session_name, deps, store, presentation) }