diff options
| author | Guillaume Melquiond | 2017-09-26 14:34:51 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-09-26 14:37:28 +0200 |
| commit | c0b244260badedf27fe2b66d3c058ad681af4371 (patch) | |
| tree | 42d2167549e386e1a809b59f9059e10322a88805 /kernel/nativelambda.mli | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
Properly display the "only" prefix for selectors (bug #5760).
This commit also fixes range selectors being incorrectly displayed.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions