aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/coq-tacindex.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/coq-tacindex.rst')
-rw-r--r--doc/sphinx/coq-tacindex.rst2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst
index 588104f465..31b2f7f8cb 100644
--- a/doc/sphinx/coq-tacindex.rst
+++ b/doc/sphinx/coq-tacindex.rst
@@ -1,3 +1,5 @@
+:orphan:
+
.. hack to get index in TOC
-------------