# HG changeset patch
# User wenzelm
# Date 1476171176 -7200
# Node ID e9b3d9c1bc5aa1a66aa2231e029891c0a7106f87
# Parent  7c51914894579b56083281cf3d18b1fde56fa7fa
support for remote tmp dirs;

diff -r 7c5191489457 -r e9b3d9c1bc5a src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 22:20:00 2016 +0200
+++ b/src/Pure/General/ssh.scala	Tue Oct 11 09:32:56 2016 +0200
@@ -277,6 +277,21 @@
       val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
       new Sftp(this, kind, options, channel)
     }
+
+
+    /* tmp dirs */
+
+    def rm_tree(remote_dir: String): Unit =
+      execute("rm -r -f " + File.bash_string(remote_dir)).check
+
+    def tmp_dir(): String =
+      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
+
+    def with_tmp_dir[A](body: String => A): A =
+    {
+      val remote_dir = tmp_dir()
+      try { body(remote_dir) } finally { rm_tree(remote_dir) }
+    }
   }
 }