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