tuned;
authorwenzelm
Thu Nov 22 17:34:30 2018 +0100 (20 months ago)
changeset 69327264b44dce6be
parent 69326 600df66ac561
child 69328 4646fcb59121
tuned;
src/Pure/General/sql.scala
     1.1 --- a/src/Pure/General/sql.scala	Thu Nov 22 15:47:58 2018 +0100
     1.2 +++ b/src/Pure/General/sql.scala	Thu Nov 22 17:34:30 2018 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4      }
     1.5  
     1.6    def string(s: String): Source =
     1.7 -    "'" + s.map(escape_char(_)).mkString + "'"
     1.8 +    s.iterator.map(escape_char(_)).mkString("'", "", "'")
     1.9  
    1.10    def ident(s: String): Source =
    1.11      Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))