# HG changeset patch
# User wenzelm
# Date 1693338875 -7200
# Node ID 193a24f78b0026120599335f491894b17501df8d
# Parent  209607465a9054a06c4a864311df92f1726163fb
proper pattern (amending ff86f10e54cd);

diff -r 209607465a90 -r 193a24f78b00 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Aug 29 20:19:57 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Aug 29 21:54:35 2023 +0200
@@ -443,7 +443,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+ \.\.\.$""")
+    val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) \(?on \S+\)? \.\.\.$""")
     val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
     val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")