--- a/src/Pure/Build/build_schedule.scala Thu Feb 15 12:42:00 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Thu Feb 15 12:48:25 2024 +0100
@@ -1035,11 +1035,11 @@
}
override def run(): Build.Results = {
- Benchmark.benchmark_requirements(build_options)
+ Build_Benchmark.benchmark_requirements(build_options)
if (build_context.jobs > 0) {
val benchmark_options = build_options.string.update("build_hostname", hostname)
- Benchmark.benchmark(benchmark_options, progress)
+ Build_Benchmark.benchmark(benchmark_options, progress)
}
_build_cluster.benchmark()