From c7cc87ef2d05706a0a40f7a2d296055cf48fc7c0 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 May 2019 19:35:17 +0200
Subject: Make progress toward #9411: reject new undefined references.

We list preexisting undefined tokens explicitly in
`doc/sphinx/conf.py` and prevent new ones from being introduced by
making it a fatal warning.

This list should be seen as a TODO. Once it is emptied, #9411 can be
closed.
---
 doc/sphinx/conf.py | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index ec3343dac6..53309cd313 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -181,7 +181,21 @@ suppress_warnings = ["misc.highlighting_failure"]
 todo_include_todos = False
 
 # Extra warnings, including undefined references
-nitpicky = False
+nitpicky = True
+
+nitpick_ignore = [ ('token', token) for token in [
+    'tactic',
+    # 142 occurrences currently sort of defined in the ltac chapter,
+    # but is it the right place?
+    'module',
+    'redexpr',
+    'modpath',
+    'dirpath',
+    'collection',
+    'term_pattern',
+    'term_pattern_string',
+    'command',
+    'symbol' ]]
 
 # -- Options for HTML output ----------------------------------------------
 
-- 
cgit v1.2.3