# 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)
         }