# HG changeset patch
# User wenzelm
# Date 1708178446 -3600
# Node ID bc6033faa22920137940f7d305df64b1833a6c65
# Parent  7a2b86a48be0b6316a31cdd50beedb84c0cf6b73
tuned;

diff -r 7a2b86a48be0 -r bc6033faa229 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Sat Feb 17 14:59:34 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Sat Feb 17 15:00:46 2024 +0100
@@ -24,7 +24,7 @@
       Options.Spec.bash_strings(options, bg = true)
   }
 
-  def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = {
+  def benchmark_requirements(options: Options, progress: Progress = new Progress): Unit = {
     val res =
       Build.build(
         options.string.update("build_engine", Build.Default_Engine.name),
@@ -33,7 +33,7 @@
     if (!res.ok) error("Failed building requirements")
   }
 
-  def benchmark(options: Options, progress: Progress = new Progress()): Unit = {
+  def benchmark(options: Options, progress: Progress = new Progress): Unit = {
     val hostname = options.string("build_hostname")
     val store = Store(options)