diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-03 00:51:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-03 00:51:54 +0200 |
| commit | 8927c6e2c42d3e9bc3650fccab093f6004fff222 (patch) | |
| tree | c5937e53430324853cdaa6a3f45bfa1803a3df81 /configure.ml | |
| parent | 5c93d722426a552f4cf1ce93bcd3dbaf14948b6f (diff) | |
[lib] Fix wrong deprecation annotations.
Introduced in #7177
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions