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 {