aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix
diff options
context:
space:
mode:
authorJim Fehrle2020-04-21 13:13:43 -0700
committerJim Fehrle2020-04-29 01:05:39 -0700
commit99e239172dbd384418500554a6d8b4a058c3545b (patch)
tree27ea776f2144b6b0f324d372ee27076198447bc4 /doc/sphinx/appendix
parent51a938a260d989f11fb1cd1d7a0205c6183f3809 (diff)
Support in-line glossary entries and references
with an index
Diffstat (limited to 'doc/sphinx/appendix')
-rw-r--r--doc/sphinx/appendix/indexes/index.rst1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
index 2ece726df7..c8b2cf46dc 100644
--- a/doc/sphinx/appendix/indexes/index.rst
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -17,6 +17,7 @@ find what you are looking for.
../../coq-optindex
../../coq-exnindex
../../coq-attrindex
+ ../../std-glossindex
For reference, here are direct links to the documentation of: