diff options
| author | Hugo Herbelin | 2020-07-29 10:44:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-05 16:19:12 +0200 |
| commit | 571834b2b43e4281ef4940ee5894d8191588bb6c (patch) | |
| tree | 4efc006b604db1cf23657053271c366683e6e8dd /kernel/nativecode.ml | |
| parent | 6d3a9220204de22e0b81dc961d2eb269128b5c2e (diff) | |
Wish #12762: warning on duplicated catch-all pattern with unused named variable.
An identifier starting with _ deactivates the warning.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions