more robust CSV syntax, e.g. for "pull_date";
authorwenzelm
Thu, 23 Jun 2022 23:42:47 +0200
changeset 75606 0f7cb6cd08fe
parent 75605 2a40ca7454bc
child 75610 da901dcafc29
child 75612 03ae0ba2aa9e
more robust CSV syntax, e.g. for "pull_date";
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