src/Pure/General/ssh.scala

--- a/src/Pure/General/ssh.scala	Fri Jun 28 11:09:58 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri Jun 28 11:37:13 2024 +0200
@@ -70,12 +70,12 @@
     val special = "[]?*\\{} \"'"
     if (str.isEmpty) "\"\""
     else if (str.exists(special.contains)) {
-      val res = new StringBuilder
-      for (c <- str) {
-        if (special.contains(c)) res += '\\'
-        res += c
+      Library.string_builder() { res =>
+        for (c <- str) {
+          if (special.contains(c)) res += '\\'
+          res += c
+        }
       }
-      res.toString()
     }
     else str
   }