src/Pure/Tools/ci_api.scala
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)
     }
   }