# HG changeset patch
# User wenzelm
# Date 1493372744 -7200
# Node ID e76d8f3e5478d4a5cbbe4d9e7216e5709411918e
# Parent  138ffa41dc540ab188c741668d3226dbc26b57fb
more standard multi-line storage in database: Prop.separator is only required for single-line meta_info within log file;

diff -r 138ffa41dc54 -r e76d8f3e5478 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Apr 28 11:29:41 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 11:45:44 2017 +0200
@@ -32,6 +32,9 @@
       if (args.isEmpty) Nil
       else List(name -> args.mkString(separator.toString))
 
+    def multiple_lines(s: String): String =
+      cat_lines(Library.space_explode(separator, s))
+
     val build_tags = SQL.Column.string("build_tags")  // multiple
     val build_args = SQL.Column.string("build_args")  // multiple
     val build_group_id = SQL.Column.string("build_group_id")
@@ -689,7 +692,7 @@
               if (c.T == SQL.Type.Date)
                 db.set_date(stmt, i + 2, meta_info.get_date(c).orNull)
               else
-                db.set_string(stmt, i + 2, meta_info.get(c).orNull)
+                db.set_string(stmt, i + 2, meta_info.get(c).map(Prop.multiple_lines(_)).orNull)
             }
 
             val n = Info.table.columns.length