tuned signature;
authorwenzelm
Tue, 07 Nov 2023 12:06:59 +0100
changeset 78910 d305af09fbad
parent 78909 65acbafc70e5
child 78911 81dab48582c6
tuned signature;
src/Pure/System/bash.scala
--- 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(" ")