src/Pure/Tools/ci_api.scala
changeset 64082 d57c7295f601
parent 64062 a7352cbde7d7
child 64106 b7ff61d50b19
     1.1 --- a/src/Pure/Tools/ci_api.scala	Fri Oct 07 11:45:30 2016 +0200
     1.2 +++ b/src/Pure/Tools/ci_api.scala	Fri Oct 07 13:58:10 2016 +0200
     1.3 @@ -45,12 +45,9 @@
     1.4      session_logs: List[(String, URL)])
     1.5    {
     1.6      def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     1.7 -    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
     1.8 -    {
     1.9 -      val text =
    1.10 -        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    1.11 -      Build_Log.Log_File(name, text).parse_session_info(name, full)
    1.12 -    }
    1.13 +    def read_log_file(name: String): Build_Log.Log_File =
    1.14 +      Build_Log.Log_File(name,
    1.15 +        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    1.16    }
    1.17  
    1.18    def build_job_builds(job_name: String): List[Job_Info] =