# HG changeset patch
# User wenzelm
# Date 1475855196 -7200
# Node ID a77c57235bae30f12fdd91c6614314616240d387
# Parent  ac7ae5067783be408490c58d28865bbd47a8269c
more uniform regexps;

diff -r ac7ae5067783 -r a77c57235bae src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 17:41:19 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 17:46:36 2016 +0200
@@ -196,10 +196,10 @@
         // workaround for jdk-8u102
         s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
 
-    val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
-    val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
-    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
-    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
+    val Test_Start = new Regex("""^Start test for .+ at (.+), (\S+)$""")
+    val Test_End = new Regex("""^End test on (.+), \S+, elapsed time:.*$""")
+    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
+    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   }
 
   private def parse_header(log_file: Log_File): Header =