From 6d9f41964a95bc6fe6d9e7d47331ac7f8574fd17 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Jul 2005 14:33:53 +0000 Subject: [PATCH] An object should be removed from disk (i.e. from the Getter scope) _before_ removing it from the environment. --- helm/matita/matitacleanLib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index d5e4c8dde..3a1d2e3db 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -141,11 +141,11 @@ let clean_baseuris ?(verbose=true) buris = debug_prerr "clean_baseuri will remove:"; if debug then List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; - List.iter (MatitaSync.remove ~verbose) l; Hashtbl.iter (fun buri _ -> MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri) ) cache_of_processed_baseuri; + List.iter (MatitaSync.remove ~verbose) l; cleaned_no := !cleaned_no + List.length l; if !cleaned_no > 30 then List.iter -- 2.39.2