# HG changeset patch
# User wenzelm
# Date 1718116637 -7200
# Node ID e5a6b3f1f3774c568ae8d4a08ef8f4f464081eae
# Parent  52154fef991d2260fb7e19738fba1101665c0551
tuned;

diff -r 52154fef991d -r e5a6b3f1f377 src/Pure/System/bash.scala
--- 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 =