# HG changeset patch
# User wenzelm
# Date 1676980102 -3600
# Node ID 05b97b54cb3b3bfaf9e55e2ea64db58cca7943df
# Parent  0231e62956a6e46e536c06407fda6c91a1534c15
tuned signature;

diff -r 0231e62956a6 -r 05b97b54cb3b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 12:42:08 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 12:48:22 2023 +0100
@@ -172,7 +172,7 @@
     running: Map[String, Build_Job] = Map.empty,
     results: Map[String, Build_Process.Result] = Map.empty
   ) {
-    def is_pending: Boolean = pending.nonEmpty
+    def finished: Boolean = pending.isEmpty
 
     def remove_pending(name: String): State =
       copy(pending = pending.flatMap(
@@ -248,7 +248,7 @@
       (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
         yield Build_Process.Entry(name, preds.toList)).toList)
 
-  protected def is_pending(): Boolean = synchronized { _state.is_pending }
+  protected def finished(): Boolean = synchronized { _state.finished }
 
   protected def next_pending(): Option[String] = synchronized {
     if (_state.running.size < (build_context.max_jobs max 1)) {
@@ -428,8 +428,12 @@
     }
 
   def run(): Map[String, Process_Result] = {
-    if (is_pending()) {
-      while (is_pending()) {
+    if (finished()) {
+      progress.echo_warning("Nothing to build")
+      Map.empty[String, Process_Result]
+    }
+    else {
+      while (!finished()) {
         if (progress.stopped) stop_running()
 
         for (job <- finished_running()) finish_job(job)
@@ -443,9 +447,5 @@
         for ((name, result) <- _state.results) yield name -> result.process_result
       }
     }
-    else {
-      progress.echo_warning("Nothing to build")
-      Map.empty[String, Process_Result]
-    }
   }
 }