author | wenzelm |
Sun, 05 Mar 2023 19:33:01 +0100 | |
changeset 77526 | e3ed231fa214 |
parent 77525 | de6fb423fd4b |
child 77527 | 790085b1002f |
--- 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 */