--- a/src/Pure/Build/build_process.scala Fri Mar 08 21:15:35 2024 +0100
+++ b/src/Pure/Build/build_process.scala Sat Mar 09 10:49:12 2024 +0100
@@ -1059,8 +1059,7 @@
val start_time_msg = build_log_verbose
val node_info = next_node_info(state, session_name)
- val node_info_msg =
- node_info.numa_node.isDefined || node_info.rel_cpus.nonEmpty || build_log_verbose
+ val node_info_msg = node_info.numa || build_log_verbose
progress.echo(
(if (store_heap) "Building " else "Running ") + session_name +
--- a/src/Pure/System/host.scala Fri Mar 08 21:15:35 2024 +0100
+++ b/src/Pure/System/host.scala Sat Mar 09 10:49:12 2024 +0100
@@ -88,6 +88,8 @@
object Node_Info { def none: Node_Info = Node_Info("", None, Nil) }
sealed case class Node_Info(hostname: String, numa_node: Option[Int], rel_cpus: List[Int]) {
+ def numa: Boolean = numa_node.isDefined || rel_cpus.nonEmpty
+
override def toString: String =
hostname +
if_proper(numa_node, "/" + numa_node.get.toString) +