src/Pure/General/ssh.scala
changeset 64306 7b6dc1b36f20
parent 64304 96bc94c87a81
child 64325 47e03cb99274
--- 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