src/Pure/General/sql.scala
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("(", ", ", ")")