# HG changeset patch
# User wenzelm
# Date 1708180052 -3600
# Node ID 7a1153c95bf978f8eb4a12302c700a4a52abaffd
# Parent  389c1bfa7c3e87e96aaf2e7c23d7a742a0637556
clarifier worker vs. master, which may coincide for local build;

diff -r 389c1bfa7c3e -r 7a1153c95bf9 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Feb 17 15:20:38 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Feb 17 15:27:32 2024 +0100
@@ -42,14 +42,16 @@
     jobs: Int = 0,
     master: Boolean = false
   ) {
-    override def toString: String =
-      "Build.Context(build_uuid = " + quote(build_uuid) + if_proper(master, ", master = true") + ")"
-
     def build_options: Options = store.options
 
     def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure
 
-    def worker_active: Boolean = jobs > 0
+    def worker: Boolean = jobs > 0
+
+    override def toString: String =
+      "Build.Context(build_uuid = " + quote(build_uuid) +
+        if_proper(worker, ", worker = true") +
+        if_proper(master, ", master = true") + ")"
   }
 
 
diff -r 389c1bfa7c3e -r 7a1153c95bf9 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Feb 17 15:20:38 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Feb 17 15:27:32 2024 +0100
@@ -1149,7 +1149,7 @@
       start_worker()
       _build_cluster.start()
 
-      if (build_context.master && !build_context.worker_active && _build_cluster.active()) {
+      if (build_context.master && !build_context.worker && _build_cluster.active()) {
         build_progress.echo("Waiting for external workers ...")
       }