diff options
| author | Maxime Dénès | 2018-02-19 10:12:00 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-19 10:12:00 +0100 |
| commit | 9accca23fb79f8a14d1cd35fa681a2e0bece1db5 (patch) | |
| tree | e2f20c83834e9956e59e0a8144e93ed4af7392b2 /dev | |
| parent | 08cbbdbcdf3456b9e1a0e688b13f431a946f3bad (diff) | |
| parent | 20916bd558a355b597337101e3281bb5ebbfcd36 (diff) | |
Merge PR #6759: detype_case predicate is not optional
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions