docs: generate index and add it to globaltoc sidebar (#6808)

This commit is contained in:
Daniel Hahler 2020-02-27 00:34:18 +01:00 committed by GitHub
parent 16c683dff9
commit f77d606d4e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 5 additions and 1 deletions

View File

@ -21,3 +21,7 @@
<hr> <hr>
{{ toc }} {{ toc }}
{%- endif %} {%- endif %}
<hr>
<a href="{{ pathto('genindex') }}">Index</a>
<hr>

View File

@ -208,7 +208,7 @@ html_sidebars = {
html_domain_indices = True html_domain_indices = True
# If false, no index is generated. # If false, no index is generated.
html_use_index = False html_use_index = True
# If true, the index is split into individual pages for each letter. # If true, the index is split into individual pages for each letter.
# html_split_index = False # html_split_index = False