--- 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)