# HG changeset patch
# User wenzelm
# Date 1708618873 -3600
# Node ID 1cd5888ec05fca7131596d01f401b735caac1fbd
# Parent  611587256801c0c104b92f3d5b234f32ba20c7fb
tuned, following 7a1153c95bf9;

diff -r 611587256801 -r 1cd5888ec05f src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Feb 22 16:31:58 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Feb 22 17:21:13 2024 +0100
@@ -1033,7 +1033,7 @@
     override def run(): Build.Results = {
       Build_Benchmark.benchmark_requirements(build_options)
 
-      if (build_context.jobs > 0) {
+      if (build_context.worker) {
         val benchmark_options = build_options.string.update("build_hostname", hostname)
         Build_Benchmark.benchmark(benchmark_options, progress)
       }