# HG changeset patch
# User wenzelm
# Date 1656020567 -7200
# Node ID 0f7cb6cd08fe6d1eaa695794e76f0e576c13660e
# Parent  2a40ca7454bcf0aa04094b2afdff4b72d5041ce1
more robust CSV syntax, e.g. for "pull_date";

diff -r 2a40ca7454bc -r 0f7cb6cd08fe src/Pure/General/csv.scala
--- a/src/Pure/General/csv.scala	Thu Jun 23 22:16:53 2022 +0200
+++ b/src/Pure/General/csv.scala	Thu Jun 23 23:42:47 2022 +0200
@@ -10,7 +10,7 @@
 object CSV {
   def print_field(field: Any): String = {
     val str = field.toString
-    if (str.exists("\",\r\n".contains(_))) {
+    if (str.exists("\",\r\n ".contains(_))) {
       (for (c <- str) yield { if (c == '"') "\"\"" else c.toString }).mkString("\"", "", "\"")
     }
     else str