# HG changeset patch
# User wenzelm
# Date 1714307316 -7200
# Node ID ead20482da9c9ec66aa0fcc19a628499f6cf73bd
# Parent  680e1618d404aa20d17d60b80c2efe14ec133bf0
build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state;

diff -r 680e1618d404 -r ead20482da9c src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Apr 26 21:32:27 2024 +0200
+++ b/src/Pure/Build/build.scala	Sun Apr 28 14:28:36 2024 +0200
@@ -121,7 +121,7 @@
 
     def build_options(options: Options, build_cluster: Boolean = false): Options = {
       val options1 = options + "completion_limit=0" + "editor_tracing_messages=0"
-      if (build_cluster) options1 + "build_database" + "build_log_verbose" else options1
+      if (build_cluster) options1 + "build_database" + "build_database_server" + "build_log_verbose" else options1  // FIXME tmp: build_database_server
     }
 
     final def build_store(options: Options,