# HG changeset patch
# User wenzelm
# Date 1699355219 -3600
# Node ID d305af09fbadb6b5734fc72efeabe4d266aadc02
# Parent  65acbafc70e524fe7805c309b2510425cc5ee635
tuned signature;

diff -r 65acbafc70e5 -r d305af09fbad 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(" ")