# HG changeset patch
# User wenzelm
# Date 1709924601 -3600
# Node ID 11fa48986f37530cc2a3ddd40d40ee81844dfe08
# Parent  56f506c556f160405b3b0ab44f2f68471ce10801
more accurate patterns --- reverting unused fc3ba0a1c82f;

diff -r 56f506c556f1 -r 11fa48986f37 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Mar 08 19:18:39 2024 +0100
+++ b/src/Pure/Admin/build_log.scala	Fri Mar 08 20:03:21 2024 +0100
@@ -452,9 +452,9 @@
     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+)\+?(\S+)\)? \.\.\.$""")
+    val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) \(?on ([^\s/]+)[^)]*\)? \.\.\.$""")
     val Session_Started3 = new Regex("""^(?:Running|Building) (\S+) \(started (\d+):(\d+):(\d+)\) \.\.\.$""")
-    val Session_Started4 = new Regex("""^(?:Running|Building) (\S+) \(started (\d+):(\d+):(\d+) on ([^\s/]+)/?(\d+)\+?(\S+)\) \.\.\.$""")
+    val Session_Started4 = new Regex("""^(?:Running|Building) (\S+) \(started (\d+):(\d+):(\d+) on ([^\s/]+)[^)]*\) \.\.\.$""")
     val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
     val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
 
@@ -501,14 +501,14 @@
         case Session_Started1(name) =>
           started += (name -> None)
 
-        case Session_Started2(name, hostname, _, _) =>
+        case Session_Started2(name, hostname) =>
           started += (name -> None)
           hostnames += (name -> hostname)
 
         case Session_Started3(name, Value.Int(t1), Value.Int(t2), Value.Int(t3)) =>
           started += (name -> Some(Time.hms(t1, t2, t3)))
 
-        case Session_Started4(name, Value.Int(t1), Value.Int(t2), Value.Int(t3), hostname, _, _) =>
+        case Session_Started4(name, Value.Int(t1), Value.Int(t2), Value.Int(t3), hostname) =>
           started += (name -> Some(Time.hms(t1, t2, t3)))
           hostnames += (name -> hostname)