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