diff -r 36547884db60 -r 7883f221d6d3 src/Pure/Build/build_cluster.scala --- 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 }