# HG changeset patch # User wenzelm # Date 1342778408 -7200 # Node ID c3192ccb0ff467fd7377b33dab5646abc53f4ff2 # Parent 63bdba7c13661b6aa35bc9e58eac218a3f0c46fe proper commas_quote; diff -r 63bdba7c1366 -r c3192ccb0ff4 src/Pure/library.scala --- 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 */