# HG changeset patch
# User wenzelm
# Date 1609071390 -3600
# Node ID b60c4ba462d4614c794e22b70a0c349e79291d6b
# Parent  83b114a6545f8960e693a6b54510ec79b8a2ae83
tuned (see also b5333fc056da);

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)
       }