# 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 */