diff options
| author | Maxime Dénès | 2017-06-14 19:00:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 19:00:23 +0200 |
| commit | e1d68573015883301cb401861e10233f6442d9ec (patch) | |
| tree | b62f4d6f0f2cfdd09cbe6080f66ec8c92024fbce /API/API.ml | |
| parent | 54063fcda793ca8179047ff2a2c9863891a97acd (diff) | |
| parent | 9a14a95f96c77ff3850d694637738358c164f4b5 (diff) | |
Merge PR#749: Normalize deprecation notices of ./configure
Diffstat (limited to 'API/API.ml')
0 files changed, 0 insertions, 0 deletions