tuned whitespace;
authorwenzelm
Sat, 24 Feb 2024 11:27:04 +0100
changeset 79718 fba02e281b44
parent 79717 da4e82434985
child 79719 8544f1045123
tuned whitespace;
src/Pure/Build/build_job.scala
src/Pure/System/host.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 =
--- 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 =>