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 f53de728c6a1ab554fed38f3bad8011c0d627f40..bab6dd2bc290a66f126e442352b580843b6da24c 100644 (file)
--- 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