# HG changeset patch
# User wenzelm
# Date 1476629889 -7200
# Node ID b1aef25ce8dfe86021339b5033d0f51657d953f1
# Parent  a4718dfc9cd4b297694555d69148b640822f596d
sftp.mkdirs according to 2a5dbad75355;

diff -r a4718dfc9cd4 -r b1aef25ce8df src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun Oct 16 16:57:48 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sun Oct 16 16:58:09 2016 +0200
@@ -150,6 +150,13 @@
     def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
     def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
 
+    def mkdirs(path: Path): Unit =
+      if (!is_dir(path)) {
+        session.execute(
+          "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
+        if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
+      }
+
     def read_dir(path: Path): List[Dir_Entry] =
     {
       val dir = channel.ls(remote_path(path))