# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701348291 -3600
# Node ID dd689c4ab688a4c45ef5e7158ab721f353dc25d9
# Parent  2d18d481c1152bea7e561dc88b784f05ac5406de
consistent hosts ordering;

diff -r 2d18d481c115 -r dd689c4ab688 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 30 13:44:21 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 30 13:44:51 2023 +0100
@@ -231,7 +231,7 @@
 
       val entries =
         if (measurements.isEmpty) {
-          val default_host = host_infos.hosts.sorted(host_infos.host_speeds).head
+          val default_host = host_infos.hosts.sorted(host_infos.host_speeds).last
           host_infos.hosts.flatMap(host =>
             dummy_entries(host, host_infos.host_factor(default_host, host)))
         }
@@ -276,7 +276,7 @@
       from.info.benchmark_score.get / to.info.benchmark_score.get
 
     val host_speeds: Ordering[Host] =
-      Ordering.fromLessThan((host1, host2) => host_factor(host1, host2) > 1)
+      Ordering.fromLessThan((host1, host2) => host_factor(host1, host2) < 1)
 
     def the_host(hostname: String): Host =
       by_hostname.getOrElse(hostname, error("Unknown host " + quote(hostname)))