# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700844724 -3600
# Node ID ff7d48e776abd1baa399cd5a3783336bc69c0bd2
# Parent  7bb8dba028ceb8fb7244007253a01b1d363b7901
properly sort entries;

diff -r 7bb8dba028ce -r ff7d48e776ab src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:24:35 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:52:04 2023 +0100
@@ -49,7 +49,9 @@
     private def hostname_factor(from: String, to: String): Double =
       host_infos.host_factor(host_infos.the_host(from), host_infos.the_host(to))
 
-    private def approximate_threads(entries: List[(Int, Time)], threads: Int): Time = {
+    private def approximate_threads(entries_unsorted: List[(Int, Time)], threads: Int): Time = {
+      val entries = entries_unsorted.sortBy(_._1)
+
       def sorted_prefix[A](xs: List[A], f: A => Long): List[A] =
         xs match {
           case x1 :: x2 :: xs =>