changeset 72012 | c81e58a81b8c |
parent 71992 | c8c3f4f0f68b |
child 72375 | e48d93811ed7 |
--- a/src/Pure/Admin/build_log.scala Sat Jul 11 14:44:50 2020 +0200 +++ b/src/Pure/Admin/build_log.scala Sat Jul 11 15:23:22 2020 +0200 @@ -644,7 +644,7 @@ task_statistics: Boolean): Session_Info = { Session_Info( - session_timing = log_file.find_props(Protocol.Timing_Marker) getOrElse Nil, + session_timing = log_file.find_props(Protocol.Session_Timing_Marker) getOrElse Nil, command_timings = if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil, theory_timings =