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,