clarified worker state: always maintain database content via worker_uuid;
authorwenzelm
Wed, 08 Mar 2023 13:36:40 +0100
changeset 77580 32f9e75c92e9
parent 77579 69d3547206db
child 77581 661d29a291ea
clarified worker state: always maintain database content via worker_uuid; clarified message;
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()
       }