+++ /dev/null
-
-
-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"
- ()
-in
-let owner =
- try
- Sys.argv.(2)
- with Invalid_argument _ -> "matita_test2"
-in
-let _ = MetadataTypes.ownerize_tables owner in
-if Sys.argv.(1) = "clean" then begin
- prerr_endline "foo";
- ignore (MetadataDb.clean ~dbd)
-end else
- let fname = Sys.argv.(1) in
- let n = ref 0 in
- let ic = open_in fname in
- try
- while true do
- let line = input_line ic in
- incr n;
- Printf.printf "%d\t%s\n" !n line; flush stdout;
- let uri = UriManager.uri_of_string line in
- MetadataDb.index_obj ~dbd ~uri
- done
- with
- | _ ->
- prerr_endline
- ("total persing time " ^
- (string_of_float !CicEnvironment.total_parsing_time));
- close_in ic
-