# HG changeset patch
# User wenzelm
# Date 1698313850 -7200
# Node ID 966aa081929fdc892de8b042352ee5bc7a5b6f3a
# Parent  ff96d94957cb9d8d96a0a3c6c099854108307d80
tuned imports;

diff -r ff96d94957cb -r 966aa081929f src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Oct 18 20:51:24 2023 +0200
+++ b/src/Pure/Tools/build_schedule.scala	Thu Oct 26 11:50:50 2023 +0200
@@ -6,7 +6,7 @@
 package isabelle
 
 
-import Host.{Info, Node_Info}
+import Host.Node_Info
 import scala.annotation.tailrec
 
 
@@ -170,7 +170,8 @@
 
   object Host_Infos {
     def dummy: Host_Infos =
-      new Host_Infos(List(Host(Info("dummy", Nil, 8, Some(1.0)), Build_Cluster.Host("dummy"))))
+      new Host_Infos(
+        List(Host(isabelle.Host.Info("dummy", Nil, 8, Some(1.0)), Build_Cluster.Host("dummy"))))
 
     def apply(build_hosts: List[Build_Cluster.Host], db: SQL.Database): Host_Infos = {
       def get_host(build_host: Build_Cluster.Host): Host = {