]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/hmysql/hMysql.ml
maxipatch for support of multiple DBs.
[helm.git] / helm / software / components / hmysql / hMysql.ml
index 374ccc600174ca450ff9da5cd65d0bd3698d63a7..b9ace8e8321a9a38275002c6bdb383a8e86a27ef 100644 (file)
@@ -39,18 +39,12 @@ exception Error of string
 
 let profiler = HExtlib.profile "mysql"
 
-let use_real_db () = 
-  not (Helm_registry.get_opt_default Helm_registry.bool
-    ~default:false "db.nodb")
-
 let quick_connect ?host ?database ?port ?password ?user () =
  profiler.HExtlib.profile 
-   (fun () -> 
-     if use_real_db () then  
-       (Some (Mysql.quick_connect ?host ?database ?port ?password ?user ())) 
-     else
-       None)
+   (fun () ->
+      Some (Mysql.quick_connect ?host ?database ?port ?password ?user ())) 
    ()
+;;
 
 let disconnect = function 
   | None -> ()
@@ -59,7 +53,7 @@ let disconnect = function
 let escape s =
  profiler.HExtlib.profile Mysql.escape s
 
-let exec dbd s =
+let exec s dbd =
   match dbd with
   | None -> None 
   | Some dbd ->