diff options
Diffstat (limited to 'doc/sphinx')
| -rwxr-xr-x | doc/sphinx/conf.py | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 1f7dd9d68..f65400e88 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -51,6 +51,10 @@ extensions = [ 'coqrst.coqdomain' ] +# Change this to "info" or "warning" to get notifications about undocumented Coq +# objects (objects with no contents). +report_undocumented_coq_objects = None + # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] |