26 def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit = |
26 def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit = |
27 hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough, |
27 hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough, |
28 dry_run = dry_run, clean = clean, filter = filter) |
28 dry_run = dry_run, clean = clean, filter = filter) |
29 |
29 |
30 progress.echo("\n* Isabelle repository:") |
30 progress.echo("\n* Isabelle repository:") |
31 sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect etc/ISABELLE_ID")) |
31 sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID")) |
32 |
32 |
33 if (!dry_run) { |
33 if (!dry_run) { |
34 Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir => |
34 Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir => |
35 val id_path = tmp_dir + Path.explode("ISABELLE_ID") |
35 val id_path = tmp_dir + Path.explode("ISABELLE_ID") |
36 File.write(id_path, isabelle_hg.id(rev = rev)) |
36 File.write(id_path, isabelle_hg.id(rev = rev)) |