diff options
Diffstat (limited to 'doc')
| -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'] |