diff options
| author | Maxime Dénès | 2018-05-14 13:43:41 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-14 13:43:41 +0200 |
| commit | 9e3989f949c1e3f20031d9af5a7bc89d97f5a951 (patch) | |
| tree | a3bc0f6a7f80840f84109460a3169726ffffe590 /doc/tools | |
| parent | 4094a8c2cac668db112fc84f5d1b287eacbf6700 (diff) | |
| parent | 805d78d12443d9df646362c024bfa83466c27fdd (diff) | |
Merge PR #7374: [sphinx] More fatal warnings.
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index f09ed4b55c..21093bd904 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -732,14 +732,14 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” - 'cmd': XRefRole(), - 'tac': XRefRole(), - 'tacn': XRefRole(), - 'opt': XRefRole(), - 'thm': XRefRole(), - 'prodn' : XRefRole(), - 'exn': XRefRole(), - 'warn': XRefRole(), + 'cmd': XRefRole(warn_dangling=True), + 'tac': XRefRole(warn_dangling=True), + 'tacn': XRefRole(warn_dangling=True), + 'opt': XRefRole(warn_dangling=True), + 'thm': XRefRole(warn_dangling=True), + 'prodn' : XRefRole(warn_dangling=True), + 'exn': XRefRole(warn_dangling=True), + 'warn': XRefRole(warn_dangling=True), # This one is special 'index': IndexXRefRole(), # These are used for highlighting |