# HG changeset patch
# User wenzelm
# Date 1678279000 -3600
# Node ID 32f9e75c92e94d21f971cef17874fca0e2f0a997
# Parent  69d3547206db54375a433b8fd7d58bc2bb6903fe
clarified worker state: always maintain database content via worker_uuid;
clarified message;

diff -r 69d3547206db -r 32f9e75c92e9 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 13:33:18 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 13:36:40 2023 +0100
@@ -144,7 +144,7 @@
       build_heap || Sessions.is_pure(name) ||
       sessions.valuesIterator.exists(_.ancestors.contains(name))
 
-    def worker: Boolean = max_jobs > 1
+    def worker_active: Boolean = max_jobs > 1
   }
 
 
@@ -921,8 +921,10 @@
     else {
       if (build_context.master) start_build()
 
-      val worker = build_context.worker
-      if (worker) start_worker() else progress.echo("Waiting for external workers ...")
+      start_worker()
+      if (build_context.master && !build_context.worker_active) {
+        progress.echo("Waiting for external workers ...")
+      }
 
       try {
         while (!finished()) {
@@ -946,7 +948,7 @@
         }
       }
       finally {
-        if (worker) stop_worker()
+        stop_worker()
         if (build_context.master) stop_build()
       }