# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700843075 -3600
# Node ID 7bb8dba028ceb8fb7244007253a01b1d363b7901
# Parent  322bcfce2b37dd86270d284455fe788cf2c3404a
tuned;

diff -r 322bcfce2b37 -r 7bb8dba028ce src/Pure/Tools/build_schedule.scala
--- 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 =