src/Pure/Tools/ci_api.scala
changeset 64041 fd454d9e97c4
parent 63992 3aa9837d05c7
child 64042 6957bd29a950
     1.1 --- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 18:26:26 2016 +0200
     1.2 +++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:26:19 2016 +0200
     1.3 @@ -45,9 +45,12 @@
     1.4      session_logs: List[(String, URL)])
     1.5    {
     1.6      def read_output(): String = Url.read(output)
     1.7 -    def read_log(full_stats: Boolean, name: String): Build.Log_Info =
     1.8 -      Build.parse_log(full_stats,
     1.9 -        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    1.10 +    def read_log(name: String, full: Boolean): Build.Session_Log_Info =
    1.11 +    {
    1.12 +      val text =
    1.13 +        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    1.14 +      Build.parse_session_log(split_lines(text), full)
    1.15 +    }
    1.16    }
    1.17  
    1.18    def build_job_builds(job_name: String): List[Build_Info] =