diff -r 83b114a6545f -r b60c4ba462d4 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Fri Dec 25 15:37:27 2020 +0000 +++ b/src/Pure/Admin/build_history.scala Sun Dec 27 13:16:30 2020 +0100 @@ -566,16 +566,16 @@ if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) { ssh.rm_tree(isabelle_repos_other) } - val other_hg = - Mercurial.clone_repository( - ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh) + + Mercurial.clone_repository( + ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh) val afp_options = if (afp_rev.isEmpty) "" else { val afp_repos = isabelle_repos_other + Path.explode("AFP") - val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh) - " -A " + Bash.string(afp_rev.get) + Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh) + " -A " + Bash.string(afp_rev.get) }