Merge PR #7556: Add a setting to warn about empty object in the refman

1 files changed, 4 insertions, 0 deletions

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 1f7dd9d689..f65400e88c 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']