changeset 65003 | 4b4ccf86755c |
parent 63791 | c6cbdfaae19e |
child 65004 | fd4d1395fa17 |
--- a/src/Pure/General/sql.scala Wed Feb 08 22:11:37 2017 +0100 +++ b/src/Pure/General/sql.scala Wed Feb 08 22:38:08 2017 +0100 @@ -32,10 +32,7 @@ quote(s.map(quote_char(_)).mkString) def quote_ident(s: String): String = - { - require(!s.contains('`')) - "`" + s + "`" - } + quote(s.replace("\"", "\"\"")) def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")