Update documentation

2022-10-20 19:55:14 +02:00 · 2022-10-20 19:55:14 +02:00 · 3173308b54
commit 3173308b54
parent 49c4040072
31 changed files with 13061 additions and 1263 deletions
--- a/_static/documentation_options.js
+++ b/_static/documentation_options.js
@ -8,5 +8,7 @@ var DOCUMENTATION_OPTIONS = {
    LINK_SUFFIX: '.html',
    HAS_SOURCE: true,
    SOURCELINK_SUFFIX: '.txt',
-    NAVIGATION_WITH_KEYS: false
+    NAVIGATION_WITH_KEYS: false,
+    SHOW_SEARCH_SUMMARY: true,
+    ENABLE_SEARCH_SHORTCUTS: true,
 };