src/Pure/Admin/build_log.scala
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 =