diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-11 09:15:39 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-17 12:48:38 +0200 |
| commit | 7f528cdb0ee42a40792d242357a239969f51cada (patch) | |
| tree | 4689d1dd9329e0c09d2ddd7c8b333a1ab3650321 /doc/sphinx/index.rst | |
| parent | b22595da96013de18f4a2bab5e6333d75a650554 (diff) | |
Add introduction and credits to the TOC.
Move credits to its own chapter (closes #6573).
Diffstat (limited to 'doc/sphinx/index.rst')
| -rw-r--r-- | doc/sphinx/index.rst | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index bd3bd93dd..f3ae49381 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -1,10 +1,7 @@ -.. _introduction: - .. include:: preamble.rst .. include:: replaces.rst .. include:: introduction.rst -.. include:: credits.rst ------------------ Table of contents @@ -23,6 +20,12 @@ Table of contents * :index:`thmindex` .. toctree:: + :caption: Preamble + + self + credits + +.. toctree:: :caption: The language language/gallina-specification-language |