# HG changeset patch
# User wenzelm
# Date 1520095053 -3600
# Node ID 56eba30e7b99f100d3144bb0798ae35a4cc114be
# Parent  9494fcf124ab1877c55e01b3be582b53ae374a87
retain latest ml_stats (amending e76c6cb0d461);

diff -r 9494fcf124ab -r 56eba30e7b99 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Mar 03 16:15:21 2018 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Mar 03 17:37:33 2018 +0100
@@ -75,7 +75,8 @@
       sessions.filter(_.head.failed).sortBy(_.name)
   }
   sealed case class Session(
-    name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics)
+    name: String, threads: Int, entries: List[Entry],
+    ml_statistics: ML_Statistics, ml_statistics_date: Long)
   {
     require(entries.nonEmpty)
 
@@ -295,8 +296,16 @@
                 errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors)))
 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
-            val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
-            val session = Session(session_name, threads, entry :: entries, ml_stats)
+            val session =
+              sessions.get(session_name) match {
+                case None =>
+                  Session(session_name, threads, List(entry), ml_stats, entry.date)
+                case Some(old) =>
+                  val (ml_stats1, ml_stats1_date) =
+                    if (entry.date > old.ml_statistics_date) (ml_stats, entry.date)
+                    else (old.ml_statistics, old.ml_statistics_date)
+                  Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
+              }
 
             if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
               data_entries += (data_name -> (sessions + (session_name -> session)))