diff options
| author | Gaëtan Gilbert | 2021-03-10 17:06:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-03-10 17:06:22 +0100 |
| commit | 2a07fb44bd453fe9ff2649b498dfb6c0e8001324 (patch) | |
| tree | d9b5030c56f12d1da6f88416883d7191803005a1 /plugins | |
| parent | cde4dceb93ba1f91d20f13a0fdea8f9731a6a626 (diff) | |
Fix kernel incorrectly assuming the "using" hyps are transitively closed
Fix #13903
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions