--- 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 =