diff options
| author | Emilio Jesus Gallego Arias | 2018-10-08 22:27:45 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-08 22:27:45 +0200 |
| commit | f3c123ea05660ce393260283d64cc3ff0eba2f8c (patch) | |
| tree | f7901e17eb87f1225df970c184773952c9085231 /dune | |
| parent | 754d9662b9f7619542e77ad85f575d227fb42b2f (diff) | |
| parent | ab237af7e952281e3fe695d888242cdf2abcaa90 (diff) | |
Merge PR #8676: Fixes #8672: ill-formed pattern substitution in notation with "let"
Diffstat (limited to 'dune')
0 files changed, 0 insertions, 0 deletions