diff -r de6fb423fd4b -r e3ed231fa214 src/Pure/System/host.scala --- a/src/Pure/System/host.scala Sun Mar 05 19:21:07 2023 +0100 +++ b/src/Pure/System/host.scala Sun Mar 05 19:33:01 2023 +0100 @@ -16,7 +16,10 @@ object Node_Info { def none: Node_Info = Node_Info("", None) } - sealed case class Node_Info(hostname: String, numa_node: Option[Int]) + sealed case class Node_Info(hostname: String, numa_node: Option[Int]) { + override def toString: String = + hostname + if_proper(numa_node, "/" + numa_node.get.toString) + } /* available NUMA nodes */