From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Jan 2008 09:58:41 +0000 (+0000)
Subject: cache for mtime of files is not polluted with None, minimal speedup
X-Git-Tag: make_still_working~5690
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=02a3fa8f07e5bb99653fcf6211e39130c27c7a98;p=helm.git

cache for mtime of files is not polluted with None, minimal speedup
---

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index f53de728c..bab6dd2bc 100644
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -162,7 +162,9 @@ module Make = functor (F:Format) -> struct
         | Some _ as x -> x
         | None ->
            match F.mtime_of_target_object b with
-           | Some t as x -> Hashtbl.add ct b x; x
+           | Some t as x -> 
+               Hashtbl.remove ct b;
+               Hashtbl.add ct b x; x
            | x -> x
       with Not_found -> assert false
     in
@@ -178,7 +180,9 @@ module Make = functor (F:Format) -> struct
         | Some _ as x -> x
         | None ->
            match F.mtime_of_target_object a with
-           | Some t as x -> Hashtbl.add ct a x; x
+           | Some t as x -> 
+               Hashtbl.remove ct b;
+               Hashtbl.add ct a x; x
            | x -> x
       with Not_found -> assert false
     in
@@ -188,7 +192,9 @@ module Make = functor (F:Format) -> struct
         | Some _ as x -> x
         | None ->
            match F.mtime_of_target_object b with
-           | Some t as x -> Hashtbl.add ct b x; x
+           | Some t as x -> 
+               Hashtbl.remove ct b;
+               Hashtbl.add ct b x; x
            | x -> x
       with Not_found -> assert false
     in