| commit | 46ed90dd014010703c7a3b2a61c4927644fa8210 | [log] [tgz] |
|---|---|---|
| author | Julien Palard <julien@palard.fr> | Wed May 29 18:34:04 2019 +0200 |
| committer | GitHub <noreply@github.com> | Wed May 29 18:34:04 2019 +0200 |
| tree | eb3b58ab720899e84bed20ab306d89c93c92dfd0 | |
| parent | 1c999262281c4a946c49614c3f8549f68049c0d9 [diff] |
Doc: Add an optional obsolete header. (GH-13638)