src/Pure/General/ssh.scala
changeset 76118 e8e3b60d8ecd
parent 76117 531248fd8952
child 76119 e5cfb05d312e
equal deleted inserted replaced
76117:531248fd8952 76118:e8e3b60d8ecd
   325 
   325 
   326     override def is_dir(path: Path): Boolean = test_entry(path, true)
   326     override def is_dir(path: Path): Boolean = test_entry(path, true)
   327     override def is_file(path: Path): Boolean = test_entry(path, false)
   327     override def is_file(path: Path): Boolean = test_entry(path, false)
   328 
   328 
   329     override def make_directory(path: Path): Path = {
   329     override def make_directory(path: Path): Path = {
   330       if (!is_dir(path)) {
   330       if (!execute("mkdir -p " + remote_path(path)).ok) {
   331         execute(
   331         error("Failed to create directory: " + quote(remote_path(path)))
   332           "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
       
   333         if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
       
   334       }
   332       }
   335       path
   333       path
   336     }
   334     }
   337 
   335 
   338     def read_dir(path: Path): List[Dir_Entry] = {
   336     def read_dir(path: Path): List[Dir_Entry] = {