author | wenzelm |
Fri, 20 Jul 2012 12:00:08 +0200 | |
changeset 48362 | c3192ccb0ff4 |
parent 48361 | 63bdba7c1366 |
child 48363 | cf081b7042d2 |
--- a/src/Pure/library.scala Fri Jul 20 11:52:20 2012 +0200 +++ b/src/Pure/library.scala Fri Jul 20 12:00:08 2012 +0200 @@ -100,7 +100,7 @@ def quote(s: String): String = "\"" + s + "\"" def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") - def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"") + def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") /* reverse CharSequence */