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