diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Tue Oct 04 20:20:21 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Tue Oct 04 21:11:35 2016 +0200 @@ -45,11 +45,11 @@ session_logs: List[(String, URL)]) { def read_output(): String = Url.read(output) - def read_log(name: String, full: Boolean): Build.Session_Log_Info = + def read_log(name: String, full: Boolean): Build_Log.Session_Info = { val text = session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" - Build.parse_session_log(name, split_lines(text), full) + Build_Log.parse_session_info(name, split_lines(text), full) } }