read relative cpu from build log;
authorFabian Huch <huch@in.tum.de>
Wed, 18 Oct 2023 20:12:07 +0200
changeset 78843 fc3ba0a1c82f
parent 78842 eb572f7b6689
child 78844 c7f436a63108
read relative cpu from build log;
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)