]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/hmysql/hMysql.ml
Bug fixed: name in letin was printed as "previous" even if given.
[helm.git] / helm / software / components / hmysql / hMysql.ml
index 76702b524f3cb95786d20d51938a5afadf09ef6f..374ccc600174ca450ff9da5cd65d0bd3698d63a7 100644 (file)
@@ -88,7 +88,6 @@ let errno = function
       | Mysql.No_such_table -> No_such_table
       | Mysql.Table_exists_error -> Table_exists_error
       | Mysql.Dup_keyname -> Dup_keyname
-      | Mysql.No_such_table -> No_such_table
       | Mysql.No_such_index -> No_such_index
       | Mysql.Bad_table_error -> Bad_table_error
       | _ -> GENERIC_ERROR "Mysql_generic_error"
@@ -96,3 +95,4 @@ let errno = function
 
 let isMysql = true
 
+let escape_string_for_like = ("ESCAPE \"\\\\\"" : ('a,'b,'c,'a) format4);;