-let _ = Helm_registry.set "getter.mode" "remote";
-let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
+
+let _ = Helm_registry.set "getter.mode" "local" in
+
+let _ = Helm_registry.set "getter.servers"
+ "file:///projects/helm/library/coq_contribs" in
+let _ = Helm_registry.set "getter.cache_dir" "." in
+let _ = Helm_registry.set "getter.maps_dir" "." in
+let _ = Helm_registry.set "getter.dtd_dir" "/projects/helm/xml/dtd" in
+
+let _ = Http_getter.init () in
+(* let _ = Http_getter.update () in *)
+
let dbd =
Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
()
let uri = UriManager.uri_of_string line in
MetadataDb.index_obj ~dbd ~uri
done
- with End_of_file -> close_in ic
+ with
+ | _ ->
+ prerr_endline
+ ("total persing time " ^ (string_of_float !CicEnvironment.total_time));
+ close_in ic