changeset 80354 | e5a6b3f1f377 |
parent 80271 | 198fc882ec0f |
--- 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 =