diff options
| author | Clément Pit-Claudel | 2018-05-17 23:42:51 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | 196f36e1db08c80c0e2d1de538a4c0fe6bae062b (patch) | |
| tree | 9e7e0fc3e6599d700b9a48fc7c25dc5d1163bdb9 /doc | |
| parent | a249f94d00c64157631fe2517d317dd75ebeff88 (diff) | |
[doc] Mark the dummy index files as orphans (the LaTeX build skips them)
Do we really need these? Wouldn't it be better to just add appropriate links to
the html template?
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/coq-cmdindex.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/coq-exnindex.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/coq-optindex.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/coq-tacindex.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/genindex.rst | 2 |
5 files changed, 10 insertions, 0 deletions
diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst index 7df6cb36c5..fd0b342ae4 100644 --- a/doc/sphinx/coq-cmdindex.rst +++ b/doc/sphinx/coq-cmdindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----------------- diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst index 100c57b085..dbf60bb06c 100644 --- a/doc/sphinx/coq-exnindex.rst +++ b/doc/sphinx/coq-exnindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ---------------------- diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst index f8046a800b..925d4cd185 100644 --- a/doc/sphinx/coq-optindex.rst +++ b/doc/sphinx/coq-optindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----------------- 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 ------------- diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index a991c7f9f8..29f792b3aa 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----- |