# HG changeset patch
# User wenzelm
# Date 1708770424 -3600
# Node ID fba02e281b4465b2874345e73cfb9daceca626b5
# Parent  da4e82434985e5364185e87b415dbca96e2286d9
tuned whitespace;

diff -r da4e82434985 -r fba02e281b44 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Sat Feb 24 11:05:11 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Sat Feb 24 11:27:04 2024 +0100
@@ -118,11 +118,9 @@
       Future.thread("build", uninterruptible = true) {
         val info = session_background.sessions_structure(session_name)
         val options = Host.node_options(info.options, node_info)
-
         val store = build_context.store
 
         using_optional(store.maybe_open_database_server(server = server)) { database_server =>
-
           store.clean_output(database_server, session_name, session_init = true)
 
           val session_sources =
diff -r da4e82434985 -r fba02e281b44 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Sat Feb 24 11:05:11 2024 +0100
+++ b/src/Pure/System/host.scala	Sat Feb 24 11:27:04 2024 +0100
@@ -67,7 +67,8 @@
 
   def node_options(options: Options, node: Node_Info): Options = {
     val threads_options =
-      if (node.rel_cpus.isEmpty) options else options.int.update("threads", node.rel_cpus.length)
+      if (node.rel_cpus.isEmpty) options
+      else options.int.update("threads", node.rel_cpus.length)
 
     node.numa_node match {
       case None if node.rel_cpus.isEmpty =>