# HG changeset patch
# User wenzelm
# Date 1542904470 -3600
# Node ID 264b44dce6bee148236930c840ad61dafb6b21d0
# Parent  600df66ac561be43a76f367ad76e910299d45c6d
tuned;

diff -r 600df66ac561 -r 264b44dce6be src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Nov 22 15:47:58 2018 +0100
+++ b/src/Pure/General/sql.scala	Thu Nov 22 17:34:30 2018 +0100
@@ -36,7 +36,7 @@
     }
 
   def string(s: String): Source =
-    "'" + s.map(escape_char(_)).mkString + "'"
+    s.iterator.map(escape_char(_)).mkString("'", "", "'")
 
   def ident(s: String): Source =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))