proper check wrt. distinct entry dates;
authorwenzelm
Fri, 07 Jul 2017 16:57:50 +0200
changeset 66254 6b5684ee07d9
parent 66253 a0cc7ebc7751
child 66256 5be685bbd16c
proper check wrt. distinct entry dates;
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 ||