src/Pure/Tools/build_log.scala
changeset 64087 a77c57235bae
parent 64086 ac7ae5067783
child 64088 210aabe359ab
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 17:41:19 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 17:46:36 2016 +0200
     1.3 @@ -196,10 +196,10 @@
     1.4          // workaround for jdk-8u102
     1.5          s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
     1.6  
     1.7 -    val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
     1.8 -    val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
     1.9 -    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
    1.10 -    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
    1.11 +    val Test_Start = new Regex("""^Start test for .+ at (.+), (\S+)$""")
    1.12 +    val Test_End = new Regex("""^End test on (.+), \S+, elapsed time:.*$""")
    1.13 +    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
    1.14 +    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
    1.15    }
    1.16  
    1.17    private def parse_header(log_file: Log_File): Header =