--- 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 = {