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 /dev/tools/pre-commit | |
| 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 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions