# HG changeset patch
# User wenzelm
# Date 1663848885 -7200
# Node ID 9d1819c28f67b79c9ac956e7c434438b9f3542d6
# Parent  5266830ee9ec19ffcb7e992f9758a8a7d7cd4592
clarified conditions: no_build is ok for presentation if "all_current" holds;
tuned;

diff -r 5266830ee9ec -r 9d1819c28f67 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 11:55:24 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 14:14:45 2022 +0200
@@ -403,10 +403,11 @@
                 }
                 val all_current = current && ancestor_results.forall(_.current)
 
-                if (all_current)
+                if (all_current) {
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
+                }
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
@@ -479,7 +480,7 @@
       }
     }
 
-    if (!no_build && !progress.stopped && results.presentation_sessions.nonEmpty) {
+    if (results.presentation_sessions.nonEmpty && !progress.stopped) {
       Browser_Info.build(browser_info, store, build_deps, results.presentation_sessions,
         progress = progress, verbose = verbose)
     }