clarified conditions: no_build is ok for presentation if "all_current" holds;
authorwenzelm
Thu, 22 Sep 2022 14:14:45 +0200
changeset 76201 9d1819c28f67
parent 76200 5266830ee9ec
child 76202 d535db35388e
clarified conditions: no_build is ok for presentation if "all_current" holds; tuned;
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)
     }