aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/persistent_cache.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-10-03 17:08:56 +0200
committerPierre-Marie Pédrot2019-10-03 17:08:56 +0200
commitac54c19e1beca7663ae7742512d110a114ce9a62 (patch)
treea96a05336c423ded9858e75fcdb96c2f150ade55 /plugins/micromega/persistent_cache.ml
parent3612ac1f639e361504cf3b2ded5609f5b643dfaa (diff)
parentb2c3eca7277ee9653e387ad3b599150b17c38572 (diff)
Merge PR #10765: Improved handling of micromega caches
Reviewed-by: Zimmi48 Reviewed-by: ppedrot Ack-by: vbgl
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
-rw-r--r--plugins/micromega/persistent_cache.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 14a1bc9712..14e2e40846 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -127,7 +127,7 @@ let open_in f =
match read_key_elem inch with
| None -> ()
| Some (key,elem) ->
- Table.replace htbl key elem ;
+ Table.add htbl key elem ;
xload () in
try
(* Locking of the (whole) file while reading *)
@@ -164,7 +164,7 @@ let add t k e =
else
let fd = descr_of_out_channel outch in
begin
- Table.replace tbl k e ;
+ Table.add tbl k e ;
do_under_lock Write fd
(fun _ ->
Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;