author | wenzelm |
Thu, 22 Nov 2018 17:34:30 +0100 | |
changeset 69327 | 264b44dce6be |
parent 69326 | 600df66ac561 |
child 69328 | 4646fcb59121 |
--- 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("\"", "\"\""))))