suppress command echo in output;
authorwenzelm
Sun, 02 Oct 2022 16:26:48 +0200
changeset 76240 30d43e9b2077
parent 76239 d042947e47a3
child 76241 aa6ce2e51e6c
suppress command echo in output;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun Oct 02 16:10:27 2022 +0200
+++ b/src/Pure/General/ssh.scala	Sun Oct 02 16:26:48 2022 +0200
@@ -214,7 +214,7 @@
     }
 
     def read_dir(path: Path): List[String] =
-      run_sftp("ls -1 -a " + sftp_path(path)).out_lines.flatMap(s =>
+      run_sftp("@ls -1 -a " + sftp_path(path)).out_lines.flatMap(s =>
         if (s == "." || s == ".." || s.endsWith("/.") || s.endsWith("/..")) None
         else Some(Library.perhaps_unprefix("./", s)))