# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710324353 -3600
# Node ID 841d0a1a9e48379fc224482f2148cd9fb753d22f
# Parent  9aef1d1535ffdaa0b4659ca6b186b3f1d87462e2
tuned;

diff -r 9aef1d1535ff -r 841d0a1a9e48 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Mar 12 13:52:29 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Wed Mar 13 11:05:53 2024 +0100
@@ -950,7 +950,7 @@
 
     private val timing_data: Timing_Data = {
       val cluster_hosts: List[Build_Cluster.Host] =
-        if (build_context.jobs == 0) build_context.build_hosts
+        if (!build_context.worker) build_context.build_hosts
         else {
           val local_build_host =
             Build_Cluster.Host(