From f77d606d4eeba38352bd3ea960f44b171fe06c1f Mon Sep 17 00:00:00 2001
From: Daniel Hahler <git@thequod.de>
Date: Thu, 27 Feb 2020 00:34:18 +0100
Subject: [PATCH] docs: generate index and add it to globaltoc sidebar (#6808)

---
 doc/en/_templates/globaltoc.html | 4 ++++
 doc/en/conf.py                   | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/doc/en/_templates/globaltoc.html b/doc/en/_templates/globaltoc.html
index 30e9da61c..4522eb2de 100644
--- a/doc/en/_templates/globaltoc.html
+++ b/doc/en/_templates/globaltoc.html
@@ -21,3 +21,7 @@
   <hr>
   {{ toc }}
 {%- endif %}
+
+<hr>
+<a href="{{ pathto('genindex') }}">Index</a>
+<hr>
diff --git a/doc/en/conf.py b/doc/en/conf.py
index 1aa1f6b0a..71f63712e 100644
--- a/doc/en/conf.py
+++ b/doc/en/conf.py
@@ -208,7 +208,7 @@ html_sidebars = {
 html_domain_indices = True
 
 # 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.
 # html_split_index = False