]> matita.cs.unibo.it Git - helm.git/commitdiff
Mysql ==> HMysql
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 26 Sep 2005 08:21:50 +0000 (08:21 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 26 Sep 2005 08:21:50 +0000 (08:21 +0000)
helm/ocaml/metadata/extractor/extractor.ml

index 8511c37d16ef55e625d6f726165badd6eb7f30cb..418d5ff7cd8b7c6e32f323942aa884bee48ce129 100644 (file)
@@ -32,7 +32,7 @@ let main () =
   Helm_registry.set "tmp.dir" path;
   Http_getter.init ();
   let dbd =
-    Mysql.quick_connect 
+    HMysql.quick_connect 
       ~host:(Helm_registry.get "db.host") 
       ~user:(Helm_registry.get "db.user") 
       ~database:(Helm_registry.get "db.database") ()