From 24da187ffe81b2509ef0307cb3360a3f7b92b80a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Nov 2020 23:20:56 +0100
Subject: Preserve sharing in the Micromega cache.

For some reason it was explicitly deactivated since the file was added, but
I have no idea why. Unsetting sharing would lead to potential explosive
memory consumption at unmarshalling time which is not worth the minimal cost
it has at marshalling time.
---
 plugins/micromega/persistent_cache.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 21178a64a5..67ceb2d9c5 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -125,7 +125,7 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
       let outch = out_channel_of_descr out in
       do_under_lock Write out (fun () ->
           Table.iter
-            (fun k e -> Marshal.to_channel outch (k, e) [Marshal.No_sharing])
+            (fun k e -> Marshal.to_channel outch (k, e) [])
             htbl;
           flush outch);
       {outch; htbl}
@@ -135,7 +135,7 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
     let fd = descr_of_out_channel outch in
     Table.add tbl k e;
     do_under_lock Write fd (fun _ ->
-        Marshal.to_channel outch (k, e) [Marshal.No_sharing];
+        Marshal.to_channel outch (k, e) [];
         flush outch)
 
   let find t k =
-- 
cgit v1.2.3