]> matita.cs.unibo.it Git - helm.git/commitdiff
An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Jul 2005 14:33:53 +0000 (14:33 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Jul 2005 14:33:53 +0000 (14:33 +0000)
from the environment.

helm/matita/matitacleanLib.ml

index d5e4c8ddeb05850e2efdb47b9bddbd2b2f85d983..3a1d2e3db5068f3af2cd02819dbcbd692827901e 100644 (file)
@@ -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