diff options
| author | Maxime Dénès | 2017-12-18 18:59:12 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 18:59:12 +0100 |
| commit | 015c9549d15e236f653b528747c1c528eff26e3c (patch) | |
| tree | 8f2922980353f648dd566fab545e3d7eaeb31757 /API/API.mli | |
| parent | 9266d34a073859f24aa615767a1311d532bba0ac (diff) | |
| parent | e4f04163d1e7c901fca1030569f8ca9d95ee4d98 (diff) | |
Merge PR #6284: Warning for absolute name masking (deprecated, should become an error)
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions