diff options
| author | Pierre-Marie Pédrot | 2020-11-16 23:20:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-24 17:58:20 +0100 |
| commit | 24da187ffe81b2509ef0307cb3360a3f7b92b80a (patch) | |
| tree | 0eda8050884d146a57cec631f4d0b062d7ac71d2 /plugins/micromega/persistent_cache.ml | |
| parent | 98dab0b2a6df19b3c179bc5fd1e211d76827a754 (diff) | |
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.
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 = |