diff options
| author | Pierre-Marie Pédrot | 2020-06-11 13:05:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-11 13:05:50 +0200 |
| commit | 149d9604c56969a067ee6d9d0d51919d96cbdc7f (patch) | |
| tree | 04357ac196a1a4535865412d5d4f06c7563d586e /dev/dune-dbg.in | |
| parent | 5611f23271be3c23761450679374690805bf51bb (diff) | |
| parent | c3dc9c558be3d3fe532d3bb3de747e920ce3e47b (diff) | |
Merge PR #12443: Fix #12442: Confusing error message when the intro pattern of "apply in" fails
Reviewed-by: ppedrot
Diffstat (limited to 'dev/dune-dbg.in')
0 files changed, 0 insertions, 0 deletions