# HG changeset patch
# User wenzelm
# Date 1663163867 -7200
# Node ID 5c971c7fc807f2d2de85f59c38ea3ef928bac4df
# Parent  ccc748255342c2454e5112084b35ec08d3e5cd0a
more robust;

diff -r ccc748255342 -r 5c971c7fc807 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Sep 14 15:42:24 2022 +0200
+++ b/src/Pure/General/ssh.scala	Wed Sep 14 15:57:47 2022 +0200
@@ -64,11 +64,12 @@
   }
 
   def sftp_string(str: String): String = {
-    val special = Set(' ', '*', '?', '{', '}')
-    if (str.exists(special)) {
+    val special = "[]?*\\{} \"'"
+    if (str.isEmpty) "\"\""
+    else if (str.exists(special.contains)) {
       val res = new StringBuilder
       for (c <- str) {
-        if (special(c)) res += '\\'
+        if (special.contains(c)) res += '\\'
         res += c
       }
       res.toString()