# HG changeset patch
# User wenzelm
# Date 1476799873 -7200
# Node ID 7b6dc1b36f2095a6ef0c5d0a4869a3c42f161a50
# Parent  4bdea66b01b8d7836bbf061dc404874bcd3a7bf9
tuned signature, in accordance to Isabelle_System;

diff -r 4bdea66b01b8 -r 7b6dc1b36f20 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Oct 18 16:08:55 2016 +0200
+++ b/src/Pure/General/ssh.scala	Tue Oct 18 16:11:13 2016 +0200
@@ -324,6 +324,8 @@
 
     /* tmp dirs */
 
+    def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
+
     def rm_tree(remote_dir: String): Unit =
       execute("rm -r -f " + Bash.string(remote_dir)).check