recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;
authorwenzelm
Thu, 22 Feb 2024 14:08:31 +0100
changeset 79699 b88d73810b50
parent 79698 b676998d7f97
child 79700 aeb53334f521
recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;
src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Feb 22 13:57:13 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Feb 22 14:08:31 2024 +0100
@@ -1213,6 +1213,11 @@
 
 
   class Build_Engine extends Build.Engine("build_schedule") {
+    override def build_options(options: Options, build_cluster: Boolean = false): Options = {
+      val options1 = super.build_options(options, build_cluster = build_cluster)
+      if (build_cluster) options1 + "build_database_server" else options1
+    }
+
     def scheduler(timing_data: Timing_Data, context: Build.Context): Scheduler = {
       val sessions_structure = context.sessions_structure