diff options
| author | Hugo Herbelin | 2018-03-29 18:30:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-03-29 18:45:46 +0200 |
| commit | 8ad6bf357284f3fcfd94f08561450bb5bf38ad36 (patch) | |
| tree | 0875a95610c22592eaf52a15bb0d9dd502aad914 /dev | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Fixes #7110 ("as" untested while looking for notation for nested patterns).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions