# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1709565657 -3600
# Node ID a478fc5cd5bde9f746558fc69f37830f9656d144
# Parent  5857bb16cf30eed3e5aeab1f8ee15043ea8faab8
partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;

diff -r 5857bb16cf30 -r a478fc5cd5bd src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Mon Mar 04 13:55:11 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Mon Mar 04 16:20:57 2024 +0100
@@ -915,6 +915,20 @@
 
     /* previous results via build log */
 
+    override def open_build_cluster(): Build_Cluster = {
+      val build_cluster = super.open_build_cluster()
+      build_cluster.init()
+
+      Build_Benchmark.benchmark_requirements(build_options)
+
+      if (build_context.worker) {
+        val benchmark_options = build_options.string("build_hostname") = hostname
+        Build_Benchmark.benchmark(benchmark_options, progress)
+      }
+
+      build_cluster.benchmark()
+    }
+
     private val timing_data: Timing_Data = {
       val cluster_hosts: List[Build_Cluster.Host] =
         if (build_context.jobs == 0) build_context.build_hosts
@@ -1030,14 +1044,6 @@
       }
 
     override def run(): Build.Results = {
-      Build_Benchmark.benchmark_requirements(build_options)
-
-      if (build_context.worker) {
-        val benchmark_options = build_options.string.update("build_hostname", hostname)
-        Build_Benchmark.benchmark(benchmark_options, progress)
-      }
-      _build_cluster.benchmark()
-
       for (db <- _build_database)
         Build_Process.private_data.transaction_lock(db, label = "Scheduler_Build_Process.init") {
           Build_Process.private_data.clean_build(db)