diff options
| author | Hugo Herbelin | 2019-12-03 00:47:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-03 01:30:24 +0100 |
| commit | 645447c1e05a95e90d09b946b322a5b587482e8e (patch) | |
| tree | d154e12819fc51590fb63977f937a791cdc6ca14 /dev | |
| parent | be04b1536fe250e8f761701f9e99650bede608d6 (diff) | |
Fixes #11231 (missing dependency in pattern-matching decompilation).
The missing dependency impacted the algorithm for detecting default
clauses.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions