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