# HG changeset patch
# User wenzelm
# Date 1707998456 -3600
# Node ID e413c94b192a399bb1b477221b9bb29d0244c3aa
# Parent  7697037f1e240f428a8015cca9c9d633561fdc59
tuned whitespace;

diff -r 7697037f1e24 -r e413c94b192a src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Thu Feb 15 12:57:19 2024 +0100
+++ b/src/Pure/Build/build.scala	Thu Feb 15 13:00:56 2024 +0100
@@ -111,8 +111,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_server" + "build_database"
-      else options1
+      if (build_cluster) options1 + "build_database_server" + "build_database" else options1
     }
 
     final def build_store(options: Options,