# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699553210 -3600
# Node ID 5553a86a1091f5f7418cf549cd1362abff1202f7
# Parent  4f940d7293ea2615ed662b38af5a874ce96a55ae
proper dummy timing entries;

diff -r 4f940d7293ea -r 5553a86a1091 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 09 17:58:21 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 09 19:06:50 2023 +0100
@@ -126,12 +126,10 @@
     def median_time(obs: List[Time]): Time = obs.sortBy(_.ms).drop(obs.length / 2).head
     def mean_time(obs: Iterable[Time]): Time = Time.ms(obs.map(_.ms).sum / obs.size)
 
-    private val dummy_entries =
+    private def dummy_entries(host: Host, host_factor: Double) =
       List(
-        Timing_Entry("dummy", "dummy", 1, Time.minutes(5)),
-        Timing_Entry("dummy", "dummy", 8, Time.minutes(1)))
-
-    def dummy: Timing_Data = new Timing_Data(dummy_entries, Host_Infos.dummy)
+        Timing_Entry("dummy", host.info.hostname, 1, Time.minutes(5).scale(host_factor)),
+        Timing_Entry("dummy", host.info.hostname, 8, Time.minutes(1).scale(host_factor)))
 
     def make(
       host_infos: Host_Infos,
@@ -150,7 +148,11 @@
         } yield (job_name, hostname, threads) -> session_info.timing.elapsed
 
       val entries =
-        if (measurements.isEmpty) dummy_entries
+        if (measurements.isEmpty) {
+          val default_host = host_infos.hosts.sorted(host_infos.host_speeds).head
+          host_infos.hosts.flatMap(host =>
+            dummy_entries(host, host_infos.host_factor(default_host, host)))
+        }
         else
           measurements.groupMap(_._1)(_._2).toList.map {
             case ((job_name, hostname, threads), timings) =>