changeset 64106 | b7ff61d50b19 |
parent 64089 | 10d719dbb3ee |
--- a/src/Pure/Tools/build_stats.scala Sat Oct 08 15:39:42 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Sat Oct 08 15:45:47 2016 +0200 @@ -29,7 +29,7 @@ val all_infos = Par_List.map((job_info: CI_API.Job_Info) => - (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos) + (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos) val all_sessions = (Set.empty[String] /: all_infos)( { case (s, (_, info)) => s ++ info.sessions.keySet })