equal
deleted
inserted
replaced
564 /* Isabelle other + AFP repository */ |
564 /* Isabelle other + AFP repository */ |
565 |
565 |
566 if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) { |
566 if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) { |
567 ssh.rm_tree(isabelle_repos_other) |
567 ssh.rm_tree(isabelle_repos_other) |
568 } |
568 } |
569 val other_hg = |
569 |
570 Mercurial.clone_repository( |
570 Mercurial.clone_repository( |
571 ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh) |
571 ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh) |
572 |
572 |
573 val afp_options = |
573 val afp_options = |
574 if (afp_rev.isEmpty) "" |
574 if (afp_rev.isEmpty) "" |
575 else { |
575 else { |
576 val afp_repos = isabelle_repos_other + Path.explode("AFP") |
576 val afp_repos = isabelle_repos_other + Path.explode("AFP") |
577 val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh) |
577 Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh) |
578 " -A " + Bash.string(afp_rev.get) |
578 " -A " + Bash.string(afp_rev.get) |
579 } |
579 } |
580 |
580 |
581 |
581 |
582 /* Admin/build_history */ |
582 /* Admin/build_history */ |
583 |
583 |