-module HGT = Http_getter_types;;
-module HG = Http_getter;;
module UM = UriManager;;
module TA = TacticAst;;
let _ =
Helm_registry.load_from "matita.conf.xml";
- HG.init ();
+ Http_getter.init ();
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove
exit 1
let _ =
- at_exit
- (fun () ->
- Http_getter_logger.log "Sync map tree to disk...";
- Http_getter.sync_dump_file ();
- print_endline "\nThanks for using Matita!\n");
if Array.length Sys.argv < 2 then usage ();
if Sys.argv.(1) = "all" then
begin