tuned;

--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:24:22 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:24:35 2023 +0100
@@ -266,6 +266,8 @@
   }
 
   class Host_Infos private(val hosts: List[Host]) {
+    require(hosts.nonEmpty)
+
     private val by_hostname = hosts.map(host => host.info.hostname -> host).toMap
 
     def host_factor(from: Host, to: Host): Double =