clarified operation: pick current pull_date instead of previous one;
authorwenzelm
Mon, 20 Nov 2023 13:08:50 +0100
changeset 79009 3641cd880bb3
parent 79008 74a4776f7a22
child 79010 aceca8baf804
clarified operation: pick current pull_date instead of previous one;
src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Nov 19 15:45:22 2023 +0000
+++ b/src/Pure/Admin/build_log.scala	Mon Nov 20 13:08:50 2023 +0100
@@ -1213,7 +1213,8 @@
       def is_empty: Boolean = entries.isEmpty
       val length: Int = entries.length
       def max(other: Run): Run = if (length >= other.length) this else other
-      def median: Option[Entry] = if (is_empty) None else Some(entries(length / 2))
+      def median: Option[Entry] =
+        if (is_empty) None else Some(entries((length - 1) / 2))
 
       override def toString: String = {
         val s = if (is_empty) "" else "length = " + length + ", median = " + median.get.pull_date