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