equal
deleted
inserted
replaced
44 timestamp: Long, |
44 timestamp: Long, |
45 main_log: URL, |
45 main_log: URL, |
46 session_logs: List[(String, String, URL)]) |
46 session_logs: List[(String, String, URL)]) |
47 { |
47 { |
48 val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin")) |
48 val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin")) |
49 val log_filename: Path = Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name)) |
49 |
|
50 def log_filename: Path = |
|
51 Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name)) |
50 |
52 |
51 def read_log_file(): Build_Log.Log_File = |
53 def read_log_file(): Build_Log.Log_File = |
52 Build_Log.Log_File(log_filename.implode, Url.read(main_log)) |
54 Build_Log.Log_File(log_filename.implode, Url.read(main_log)) |
53 |
55 |
54 def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] = |
56 def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] = |