# HG changeset patch
# User wenzelm
# Date 1700482130 -3600
# Node ID 3641cd880bb36c489c1f37a16179a6a84aa9be76
# Parent  74a4776f7a222dd37dcef12c54ad18971ca2adbf
clarified operation: pick current pull_date instead of previous one;

diff -r 74a4776f7a22 -r 3641cd880bb3 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