# HG changeset patch
# User wenzelm
# Date 1499439470 -7200
# Node ID 6b5684ee07d9fc396b2d4504e723dd95bade4af2
# Parent  a0cc7ebc7751cd779e2f69c04b5600d3bd955851
proper check wrt. distinct entry dates;

diff -r a0cc7ebc7751 -r 6b5684ee07d9 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Fri Jul 07 11:32:06 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Fri Jul 07 16:57:50 2017 +0200
@@ -82,10 +82,12 @@
     def order: Long = - head.timing.elapsed.ms
 
     def finished_entries: List[Entry] = entries.filter(_.finished)
+    def finished_entries_size: Int =
+      finished_entries.map(entry => entry.pull_date.unix_epoch).toSet.size
 
-    def check_timing: Boolean = finished_entries.length >= 3
+    def check_timing: Boolean = finished_entries_size >= 3
     def check_heap: Boolean =
-      finished_entries.length >= 3 &&
+      finished_entries_size >= 3 &&
       finished_entries.forall(entry =>
         entry.maximum_heap > 0 ||
         entry.average_heap > 0 ||