src/Pure/Tools/ci_api.scala
changeset 64045 c6160d0b0337
parent 64042 6957bd29a950
child 64054 1fc9ab31720d
     1.1 --- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 20:20:21 2016 +0200
     1.2 +++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 21:11:35 2016 +0200
     1.3 @@ -45,11 +45,11 @@
     1.4      session_logs: List[(String, URL)])
     1.5    {
     1.6      def read_output(): String = Url.read(output)
     1.7 -    def read_log(name: String, full: Boolean): Build.Session_Log_Info =
     1.8 +    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
     1.9      {
    1.10        val text =
    1.11          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    1.12 -      Build.parse_session_log(name, split_lines(text), full)
    1.13 +      Build_Log.parse_session_info(name, split_lines(text), full)
    1.14      }
    1.15    }
    1.16