From: Andrea Asperti Date: Mon, 26 Sep 2005 08:21:50 +0000 (+0000) Subject: Mysql ==> HMysql X-Git-Tag: LAST_BEFORE_NEW~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0db45531321453e765eaeccb1a0b8c774a4d0c1;p=helm.git Mysql ==> HMysql --- diff --git a/helm/ocaml/metadata/extractor/extractor.ml b/helm/ocaml/metadata/extractor/extractor.ml index 8511c37d1..418d5ff7c 100644 --- a/helm/ocaml/metadata/extractor/extractor.ml +++ b/helm/ocaml/metadata/extractor/extractor.ml @@ -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") ()