From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Jul 2005 14:33:53 +0000 (+0000)
Subject: An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
X-Git-Tag: V_0_7_2~102
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d9f41964a95bc6fe6d9e7d47331ac7f8574fd17;p=helm.git

An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
from the environment.
---

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