diff options
| author | Emilio Jesus Gallego Arias | 2019-12-09 04:19:11 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-09 11:32:32 +0100 |
| commit | 6e505f039ca4583f75f57a340e155666d7115241 (patch) | |
| tree | 3ec6100ad5299a1d897026eb3b21033944d7494f /dev/db | |
| parent | 1f4f00062b83b88114657223895bb1a367bc3cff (diff) | |
[hashset] Don't use deprecated Obj.truncate
We follow the solution used upstream
https://github.com/ocaml/ocaml/pull/2279
Fixes half of #10602
Diffstat (limited to 'dev/db')
0 files changed, 0 insertions, 0 deletions