diff options
| author | Vincent Laporte | 2019-05-03 13:41:47 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-03 13:41:47 +0000 |
| commit | a37d1c0e433f34d0ab5357b1f78eb0e04d961dc8 (patch) | |
| tree | d986ebd93114b8b29711e8afc1811683905d4812 /kernel/nativecode.ml | |
| parent | 6960da4736186fa6214854329f36f558e7aa4d0b (diff) | |
| parent | 24c570834dccc90c7ff14d3f6b9d33b818fa79c9 (diff) | |
Merge PR #10025: Fix #9994: `revert dependent` is extremely slow.
Ack-by: ppedrot
Reviewed-by: vbgl
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions