diff options
| author | Gaëtan Gilbert | 2019-11-22 14:13:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-22 14:13:34 +0100 |
| commit | 11337dac57824fc96c91cba7c4d0bc6d1c068068 (patch) | |
| tree | 2bbd2fce29175e30c9b5d4629df759463c5cfd21 /kernel/nativecode.mli | |
| parent | 27e4f306d54f2cc04b40d740584a7b3eda2d490a (diff) | |
Add test for #11161
This is better than expecting other tests to fail if we mess up again.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions