diff options
| author | Maxime Dénès | 2017-04-19 09:24:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-19 09:24:51 +0200 |
| commit | 39197cf220afe157254ebc9cae52a36516148a95 (patch) | |
| tree | 842997df3951ca4b7ed30bc035e76d1b2a62c843 /dev/include | |
| parent | a53e846fbc4a03527383244d706fc37d4816d979 (diff) | |
| parent | 0cd64f60b1057e4c3daa0523ed42b00c315cf136 (diff) | |
Merge PR#545: Add some hints to the "real" database to automatically discharge literal comparisons.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions