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