diff options
| author | Florian Diebold <[email protected]> | 2021-05-15 16:01:27 +0100 |
|---|---|---|
| committer | Florian Diebold <[email protected]> | 2021-05-21 16:48:34 +0100 |
| commit | 32fc944263ae0b30eba130fbcf28f4eb5578fdb3 (patch) | |
| tree | 779b701955168f7472a5ae7e760cb95c6ca604e4 /editors | |
| parent | a09079f27aa631b011f6c0703200862d28af81f4 (diff) | |
Fix handling of diverging branches in match coercion
Fixes #7626.
Diffstat (limited to 'editors')
0 files changed, 0 insertions, 0 deletions