]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/hmysql/hMysql.ml
HSql.Error ==> HSql.Error of string
[helm.git] / helm / software / components / hmysql / hMysql.ml
index 041f4392287bf0642a1d50a20259d5efa8c110cb..76702b524f3cb95786d20d51938a5afadf09ef6f 100644 (file)
@@ -35,7 +35,7 @@ type error_code =
  | No_such_index
  | Bad_table_error
  | GENERIC_ERROR of string
-exception Error
+exception Error of string
 
 let profiler = HExtlib.profile "mysql"
 
@@ -65,7 +65,7 @@ let exec dbd s =
   | Some dbd -> 
      try 
       Some (profiler.HExtlib.profile (Mysql.exec dbd) s)
-     with Mysql.Error _ -> raise Error
+     with Mysql.Error s -> raise (Error s)
 
 let map res ~f =
   match res with