--- a/src/Pure/Admin/build_log.scala Wed Oct 18 20:07:54 2023 +0200
+++ b/src/Pure/Admin/build_log.scala Wed Oct 18 20:12:07 2023 +0200
@@ -444,7 +444,7 @@
val Session_Timing =
new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
val Session_Started1 = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
- val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) \(?on ([^\s/]+)/?(\d+)\)? \.\.\.$""")
+ val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) \(?on ([^\s/]+)/?(\d+)\+?(\S+)\)? \.\.\.$""")
val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
@@ -491,7 +491,7 @@
case Session_Started1(name) =>
started += name
- case Session_Started2(name, hostname, numa_node) =>
+ case Session_Started2(name, hostname, numa_node, rel_cpus) =>
started += name
hostnames += (name -> hostname)