178 lazy val build_cluster_isabelle: Other_Isabelle = |
178 lazy val build_cluster_isabelle: Other_Isabelle = |
179 Other_Isabelle(built_cluster_isabelle_home, |
179 Other_Isabelle(built_cluster_isabelle_home, |
180 isabelle_identifier = build_cluster_identifier, ssh = ssh) |
180 isabelle_identifier = build_cluster_identifier, ssh = ssh) |
181 |
181 |
182 def sync(): Other_Isabelle = { |
182 def sync(): Other_Isabelle = { |
183 Sync.sync(options, Rsync.Context(ssh = ssh), built_cluster_isabelle_home, |
183 val context = Rsync.Context(ssh = ssh) |
184 purge_heaps = true, |
184 val target = built_cluster_isabelle_home |
185 preserve_jars = true, |
185 if (Mercurial.Hg_Sync.ok(Path.ISABELLE_HOME)) { |
186 dirs = Sync.afp_dirs(build_context.afp_root)) |
186 val source = File.standard_path(Path.ISABELLE_HOME) |
|
187 Rsync.exec(context, clean = true, |
|
188 args = List("--", Url.direct_path(source), context.target(target))).check |
|
189 } |
|
190 else { |
|
191 Sync.sync(options, context, target, |
|
192 purge_heaps = true, |
|
193 preserve_jars = true, |
|
194 dirs = Sync.afp_dirs(build_context.afp_root)) |
|
195 } |
187 build_cluster_isabelle |
196 build_cluster_isabelle |
188 } |
197 } |
189 |
198 |
190 def init(): Unit = |
199 def init(): Unit = |
191 build_cluster_isabelle.init(other_settings = |
200 build_cluster_isabelle.init(other_settings = |