]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/library/libraryClean.ml
milestone in basic_2 with additions in static_2
[helm.git] / matita / components / library / libraryClean.ml
index 6f58bb54eaadb79274c1cca29328b1a7b4aaab0f..8d78189920c8db5f6c68e9449b476aed3c10b71a 100644 (file)
@@ -220,10 +220,11 @@ let moo_root_dir = lazy (
 *)
 
 let rec close_db cache_of_processed_baseuri uris next =
-  prerr_endline "CLOSE_DB "; uris (* MATITA 1.0 *)
+  uris (* MATITA 1.0 *)
 ;;
 
 let clean_baseuris ?(verbose=true) buris =
+ (* MATITA 1.0 *) () (*
   let cache_of_processed_baseuri = Hashtbl.create 1024 in
   let buris = List.map Http_getter_misc.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
@@ -248,3 +249,4 @@ let clean_baseuris ?(verbose=true) buris =
      with Http_getter_types.Key_not_found _ -> ())
    (HExtlib.list_uniq (List.fast_sort Pervasives.compare
      (List.map NUri.baseuri_of_uri l @ buris)))
+*)