- (List.map (UriManager.buri_of_uri) l @ buris)));
- List.iter
- (let last_baseuri = ref "" in
- fun uri ->
- let buri = UriManager.buri_of_uri uri in
- if buri <> !last_baseuri then
- begin
- if not (Helm_registry.get_bool "matita.verbose") then
- (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
- else
- HLog.message ("Removing: " ^ buri ^ "/*");
- last_baseuri := buri
- end;
- LibrarySync.remove_obj uri
- ) l;
- if HSql.isMysql dbtype dbd then
- begin
- cleaned_no := !cleaned_no + List.length l;
- if !cleaned_no > 30 && HSql.isMysql dbtype dbd then
- begin
- cleaned_no := 0;
- List.iter
- (function table ->
- ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table)))
- [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
- MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
- MetadataTypes.count_tbl()]
- end
- end
- *)