--- 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()