src/Pure/Tools/ci_api.scala
changeset 64106 b7ff61d50b19
parent 64082 d57c7295f601
     1.1 --- a/src/Pure/Tools/ci_api.scala	Sat Oct 08 15:39:42 2016 +0200
     1.2 +++ b/src/Pure/Tools/ci_api.scala	Sat Oct 08 15:45:47 2016 +0200
     1.3 @@ -44,8 +44,8 @@
     1.4      output: URL,
     1.5      session_logs: List[(String, URL)])
     1.6    {
     1.7 -    def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     1.8 -    def read_log_file(name: String): Build_Log.Log_File =
     1.9 +    def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
    1.10 +    def read_session_log(name: String): Build_Log.Log_File =
    1.11        Build_Log.Log_File(name,
    1.12          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    1.13    }