diff options
author | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-13 12:18:38 -0400 |
---|---|---|
committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-22 11:40:13 -0400 |
commit | 9811cda7698652b51e8ebdb25db7285ab8e5ae9a (patch) | |
tree | 05ee79403aa9b5dfb62bb7a5f7b1137d3e483ab7 /doc/sphinx/preamble.rst | |
parent | 55c35435dc383a3f488a706605ba57607fd88681 (diff) |
[doc] Document the new report_undocumented_coq_objects setting
Diffstat (limited to 'doc/sphinx/preamble.rst')
0 files changed, 0 insertions, 0 deletions