diff options
| author | Emilio Jesus Gallego Arias | 2019-05-24 00:45:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-24 00:45:40 +0200 |
| commit | 48bda9d680f605f012eb9c3af61f9e076a7d51be (patch) | |
| tree | 6d86a4ed1f3f5d54aeeaf9e55d35d9d3813496bc /kernel/nativelambda.mli | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
| parent | 7c82a2713c8827ebc1e2896c83c6e7bd2f81c063 (diff) | |
Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions