clarified operation: avoid perl;
authorwenzelm
Sun, 11 Sep 2022 23:48:17 +0200
changeset 76118 e8e3b60d8ecd
parent 76117 531248fd8952
child 76119 e5cfb05d312e
clarified operation: avoid perl;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun Sep 11 23:37:05 2022 +0200
+++ b/src/Pure/General/ssh.scala	Sun Sep 11 23:48:17 2022 +0200
@@ -327,10 +327,8 @@
     override def is_file(path: Path): Boolean = test_entry(path, false)
 
     override def make_directory(path: Path): Path = {
-      if (!is_dir(path)) {
-        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)))
+      if (!execute("mkdir -p " + remote_path(path)).ok) {
+        error("Failed to create directory: " + quote(remote_path(path)))
       }
       path
     }