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 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 |
584 ssh.with_tmp_dir(tmp_dir => |
584 ssh.with_tmp_dir(tmp_dir => |
585 { |
585 { |
586 val output_file = tmp_dir + Path.explode("output") |
586 val output_file = tmp_dir + Path.explode("output") |
587 |
587 |
588 execute("Admin/build_history", |
588 val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id) |
589 "-o " + ssh.bash_path(output_file) + |
589 |
590 (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " + |
590 try { |
591 options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args, |
591 execute("Admin/build_history", |
592 echo = true, strict = false) |
592 "-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " + |
|
593 ssh.bash_path(isabelle_repos_other) + " " + args, |
|
594 echo = true, strict = false) |
|
595 } |
|
596 catch { |
|
597 case ERROR(msg) => |
|
598 cat_error(msg, |
|
599 "The error(s) above occurred for build_bistory " + rev_options + afp_options) |
|
600 } |
593 |
601 |
594 for (line <- split_lines(ssh.read(output_file))) |
602 for (line <- split_lines(ssh.read(output_file))) |
595 yield { |
603 yield { |
596 val log = Path.explode(line) |
604 val log = Path.explode(line) |
597 val bytes = ssh.read_bytes(log) |
605 val bytes = ssh.read_bytes(log) |