# HG changeset patch
# User wenzelm
# Date 1664720808 -7200
# Node ID 30d43e9b2077def4921ba2361b38b52ca0d9a1db
# Parent  d042947e47a33afeac630ad0faa6a44e3e7a0b06
suppress command echo in output;

diff -r d042947e47a3 -r 30d43e9b2077 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)))