# HG changeset patch # User Fabian Huch # Date 1710326720 -3600 # Node ID c00181ecf8697c12d5b707d0b7ed0bcea8c51dab # Parent 841d0a1a9e48379fc224482f2148cd9fb753d22f remove unused dummy; diff -r 841d0a1a9e48 -r c00181ecf869 src/Pure/Build/build_schedule.scala --- a/src/Pure/Build/build_schedule.scala Wed Mar 13 11:05:53 2024 +0100 +++ b/src/Pure/Build/build_schedule.scala Wed Mar 13 11:45:20 2024 +0100 @@ -339,10 +339,6 @@ } object Host_Infos { - def dummy: Host_Infos = - new Host_Infos( - List(Host(isabelle.Host.Info("dummy", Nil, 8, Some(1.0)), Build_Cluster.Host("dummy")))) - def load(build_hosts: List[Build_Cluster.Host], db: SQL.Database): Host_Infos = { def get_host(build_host: Build_Cluster.Host): Host = { val info =