# HG changeset patch
# User wenzelm
# Date 1708607311 -3600
# Node ID b88d73810b50d1c64efc99295bb37f89eb6d32af
# Parent  b676998d7f97d1593b6602cf9a5bea67de4697c9
recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;

diff -r b676998d7f97 -r b88d73810b50 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