diff options
| author | Emilio Jesus Gallego Arias | 2018-03-04 20:11:03 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-09 23:48:15 +0100 |
| commit | c803bb6cc31134f0759ecf06d5411ce812e05e54 (patch) | |
| tree | dc70ab174df5dd753b68fc51f2e4afd7e54d85c5 /dev/include | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
[doc] Document removal of deprecated options.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions