diff -r c157af5f346e -r fd24f380b588 src/Pure/Tools/build_cluster.scala --- a/src/Pure/Tools/build_cluster.scala Thu Jul 20 12:55:47 2023 +0200 +++ b/src/Pure/Tools/build_cluster.scala Fri Jul 21 10:56:11 2023 +0200 @@ -110,7 +110,7 @@ // class extensible via Build.Engine.build_process() and Build_Process.init_cluster() class Build_Cluster( - build_context: Build_Process.Context, + build_context: Build.Context, remote_hosts: List[Build_Cluster.Host], progress: Progress = new Progress ) extends AutoCloseable {