--- a/src/Pure/General/ssh.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/General/ssh.scala Tue Oct 18 16:03:30 2016 +0200
@@ -243,6 +243,7 @@
}
def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
+ def bash_path(path: Path): String = Bash.string(remote_path(path))
def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
@@ -324,7 +325,7 @@
/* tmp dirs */
def rm_tree(remote_dir: String): Unit =
- execute("rm -r -f " + File.bash_string(remote_dir)).check
+ execute("rm -r -f " + Bash.string(remote_dir)).check
def tmp_dir(): String =
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out