diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-03 19:06:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-03 19:06:41 +0200 |
| commit | 7a59d74a8ccb62a68f0b1e460bdc39041345eba8 (patch) | |
| tree | 290d5635903a60658dfd9f19e5d00eec79027b48 /library | |
| parent | c5d6b26e8de1a32054509d11ddeeaba3b8bfd8ac (diff) | |
| parent | 47d4276763971f155c81f4e299d855883b6c9408 (diff) | |
Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns with different variables
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions