# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700843062 -3600
# Node ID 322bcfce2b37dd86270d284455fe788cf2c3404a
# Parent  cd7c1acc9cf28684417261b34a03bbb5c96e833a
tuned;

diff -r cd7c1acc9cf2 -r 322bcfce2b37 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:06:32 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:24:22 2023 +0100
@@ -203,7 +203,7 @@
   }
 
   object Timing_Data {
-    def median_time(obs: List[Time]): Time = obs.sortBy(_.ms).drop(obs.length / 2).head
+    def median_time(obs: List[Time]): Time = obs.sortBy(_.ms).apply(obs.length / 2)
     def mean_time(obs: Iterable[Time]): Time = Time.ms(obs.map(_.ms).sum / obs.size)
 
     private def dummy_entries(host: Host, host_factor: Double) =