diff options
| author | Théo Zimmermann | 2017-07-04 17:11:45 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-07-11 16:27:56 +0200 |
| commit | fbbcea2eda411fbacfafdeec3266a19af17935f3 (patch) | |
| tree | 24c4d298f6a0a5f294518c450d0dc98f59417bd3 /API/API.mli | |
| parent | ba7129f547d1f06c7eb67412404445681d22b920 (diff) | |
Deprecate options that were introduced for compatibility with 8.5.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions