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(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) |
47 def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) |
48 def read_log(name: String, full: Boolean): Build_Log.Session_Info = |
48 def read_log_file(name: String): Build_Log.Log_File = |
49 { |
49 Build_Log.Log_File(name, |
50 val text = |
50 session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "") |
51 session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" |
|
52 Build_Log.Log_File(name, text).parse_session_info(name, full) |
|
53 } |
|
54 } |
51 } |
55 |
52 |
56 def build_job_builds(job_name: String): List[Job_Info] = |
53 def build_job_builds(job_name: String): List[Job_Info] = |
57 { |
54 { |
58 val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") |
55 val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") |