--- 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