equal
deleted
inserted
replaced
43 timestamp: Long, |
43 timestamp: Long, |
44 output: URL, |
44 output: URL, |
45 session_logs: List[(String, URL)]) |
45 session_logs: List[(String, URL)]) |
46 { |
46 { |
47 def read_output(): String = Url.read(output) |
47 def read_output(): String = Url.read(output) |
48 def read_log(full_stats: Boolean, name: String): Build.Log_Info = |
48 def read_log(name: String, full: Boolean): Build.Session_Log_Info = |
49 Build.parse_log(full_stats, |
49 { |
50 session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "") |
50 val text = |
|
51 session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" |
|
52 Build.parse_session_log(split_lines(text), full) |
|
53 } |
51 } |
54 } |
52 |
55 |
53 def build_job_builds(job_name: String): List[Build_Info] = |
56 def build_job_builds(job_name: String): List[Build_Info] = |
54 { |
57 { |
55 val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") |
58 val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") |