diff options
| author | Hugo Herbelin | 2016-10-19 17:20:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-19 17:21:09 +0200 |
| commit | 00978cddf6e2da71892de6362e69c372429e159f (patch) | |
| tree | 1f89494f1e08bcabd4924ebbe1506bc86c843a3e /dev | |
| parent | 21e1d501e17c9989d9cd689988a510e1864f817a (diff) | |
Test for variant of #5142 (good error message on pattern-matching failure).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions