diff -r d93bd6d253c6 -r b7ff61d50b19 src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Sat Oct 08 15:39:42 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Sat Oct 08 15:45:47 2016 +0200 @@ -44,8 +44,8 @@ output: URL, session_logs: List[(String, URL)]) { - def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) - def read_log_file(name: String): Build_Log.Log_File = + def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) + def read_session_log(name: String): Build_Log.Log_File = Build_Log.Log_File(name, session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "") }