tuned;

--- a/src/Pure/System/bash.scala	Tue Jun 11 16:32:10 2024 +0200
+++ b/src/Pure/System/bash.scala	Tue Jun 11 16:37:17 2024 +0200
@@ -36,7 +36,7 @@
   }
 
   def string(s: String): String =
-    if (s == "") "\"\""
+    if (s.isEmpty) "\"\""
     else UTF8.bytes(s).iterator.map(bash_chr).mkString
 
   def strings(ss: Iterable[String]): String =