tuned;

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