# HG changeset patch
# User wenzelm
# Date 1497710205 -7200
# Node ID 8c8e77dbe6fec6b1bf09d272b55d8ef98e8f0280
# Parent  b5333fc056da365085380677a8510456c73e6184
more robust: do not touch unrelated directory isabelle_repos_other (i.e. bad argument);

diff -r b5333fc056da -r 8c8e77dbe6fe src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jun 17 16:28:16 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jun 17 16:36:45 2017 +0200
@@ -460,7 +460,9 @@
       ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
     }
 
-    ssh.rm_tree(isabelle_repos_other)
+    if (Mercurial.is_repository(isabelle_repos_other, ssh = Some(ssh))) {
+      ssh.rm_tree(isabelle_repos_other)
+    }
     val other_hg =
       Mercurial.clone_repository(
         ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = Some(ssh))