author | wenzelm |
Tue, 07 Nov 2023 12:06:59 +0100 | |
changeset 78910 | d305af09fbad |
parent 78909 | 65acbafc70e5 |
child 78911 | 81dab48582c6 |
--- a/src/Pure/System/bash.scala Tue Nov 07 12:06:50 2023 +0100 +++ b/src/Pure/System/bash.scala Tue Nov 07 12:06:59 2023 +0100 @@ -39,7 +39,7 @@ if (s == "") "\"\"" else UTF8.bytes(s).iterator.map(bash_chr).mkString - def strings(ss: List[String]): String = + def strings(ss: Iterable[String]): String = ss.iterator.map(Bash.string).mkString(" ")