# HG changeset patch
# User wenzelm
# Date 1486589888 -3600
# Node ID 4b4ccf86755c6c4c677a68a3d58d11723672bf92
# Parent  0c44e3e9126f749e83276ca7df2a3b9d180bda01
more portable: SQL standard syntax instead of MySQL extension;

diff -r 0c44e3e9126f -r 4b4ccf86755c src/Pure/General/sql.scala
--- 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("(", ", ", ")")