prefer static object, while class is required for "services" (see 47eb96592aa2);
authorwenzelm
Thu, 15 Feb 2024 12:57:19 +0100
changeset 79621 7697037f1e24
parent 79620 3914bca631b9
child 79622 e413c94b192a
prefer static object, while class is required for "services" (see 47eb96592aa2);
src/Pure/Build/build.scala
src/Pure/Build/build_benchmark.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 */
--- 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)