src/Pure/Tools/ci_api.scala
changeset 64042 6957bd29a950
parent 64041 fd454d9e97c4
child 64045 c6160d0b0337
     1.1 --- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:26:19 2016 +0200
     1.2 +++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:38:43 2016 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4      {
     1.5        val text =
     1.6          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
     1.7 -      Build.parse_session_log(split_lines(text), full)
     1.8 +      Build.parse_session_log(name, split_lines(text), full)
     1.9      }
    1.10    }
    1.11