# 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