diff options
| author | Théo Zimmermann | 2018-11-26 09:36:11 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-14 09:14:47 +0100 |
| commit | ac5c18106592bd97d05b5125039394a98aebec57 (patch) | |
| tree | 88dac53e8b1ccf0be36b6bd6498d33e6b7380b3c | |
| parent | 584fcd368401d33f0a8215f21c6f56dc8dc612d9 (diff) | |
Turn warning on for undocumented objects. Closes #7602.
| -rwxr-xr-x | doc/sphinx/conf.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index e681d0f3ff..39047f4f23 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -61,7 +61,7 @@ extensions = [ # Change this to "info" or "warning" to get notifications about undocumented Coq # objects (objects with no contents). -report_undocumented_coq_objects = None +report_undocumented_coq_objects = "warning" # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] |