support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");

--- a/src/Pure/Build/build_cluster.scala	Sat May 25 19:42:09 2024 +0200
+++ b/src/Pure/Build/build_cluster.scala	Sat May 25 20:08:01 2024 +0200
@@ -180,10 +180,19 @@
         isabelle_identifier = build_cluster_identifier, ssh = ssh)
 
     def sync(): Other_Isabelle = {
-      Sync.sync(options, Rsync.Context(ssh = ssh), built_cluster_isabelle_home,
-        purge_heaps = true,
-        preserve_jars = true,
-        dirs = Sync.afp_dirs(build_context.afp_root))
+      val context = Rsync.Context(ssh = ssh)
+      val target = built_cluster_isabelle_home
+      if (Mercurial.Hg_Sync.ok(Path.ISABELLE_HOME)) {
+        val source = File.standard_path(Path.ISABELLE_HOME)
+        Rsync.exec(context, clean = true,
+          args = List("--", Url.direct_path(source), context.target(target))).check
+      }
+      else {
+        Sync.sync(options, context, target,
+          purge_heaps = true,
+          preserve_jars = true,
+          dirs = Sync.afp_dirs(build_context.afp_root))
+      }
       build_cluster_isabelle
     }