# HG changeset patch
# User wenzelm
# Date 1707998239 -3600
# Node ID 7697037f1e240f428a8015cca9c9d633561fdc59
# Parent  3914bca631b93f603e6fd91ff4a3dac765c09a6f
prefer static object, while class is required for "services" (see 47eb96592aa2);

diff -r 3914bca631b9 -r 7697037f1e24 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Thu Feb 15 12:48:25 2024 +0100
+++ b/src/Pure/Build/build.scala	Thu Feb 15 12:57:19 2024 +0100
@@ -143,6 +143,7 @@
   }
 
   class Default_Engine extends Engine("") { override def toString: String = "<default>" }
+  object Default_Engine extends Default_Engine
 
 
   /* build */
diff -r 3914bca631b9 -r 7697037f1e24 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Thu Feb 15 12:48:25 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Thu Feb 15 12:57:19 2024 +0100
@@ -25,7 +25,7 @@
   def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = {
     val res =
       Build.build(
-        options.string.update("build_engine", Build.Default_Engine().name),
+        options.string.update("build_engine", Build.Default_Engine.name),
         selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)),
         progress = progress, build_heap = true)
     if (!res.ok) error("Failed building requirements")
@@ -44,7 +44,7 @@
         val full_sessions = Sessions.load_structure(options.int.update("threads", 1))
 
         val build_context =
-          Build.Context(store, new Build.Default_Engine,
+          Build.Context(store, Build.Default_Engine,
             Sessions.deps(full_sessions.selection(selection)).check_errors)
 
         val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)