# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1697652727 -7200
# Node ID fc3ba0a1c82f622cc709f2e64869a4afae885b44
# Parent  eb572f7b668981a3083663e782810953efe046d8
read relative cpu from build log;

diff -r eb572f7b6689 -r fc3ba0a1c82f src/Pure/Admin/build_log.scala
--- 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)