diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 08:37:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-22 11:33:58 +0100 |
| commit | bf1e64fc3a79e2eff49aaeeaa966516b11f1cd9f (patch) | |
| tree | 8d1fcf957a7ec890a4a25873f7d53f2d62cc6ba0 /library/lib.ml | |
| parent | 88afd8a9853c772b6b1681c7ae208e55e7daacbe (diff) | |
[api] Re-enable deprecation warnings.
With a bit of care we can enable full deprecation warnings again in
this funny file.
Diffstat (limited to 'library/lib.ml')
0 files changed, 0 insertions, 0 deletions