Sphinx: listing unused RTD theme options

Options are still commented out.
AdaCore · Oct 6, 2023 · 1dd70cb · 1dd70cb
1 parent 4e00941
commit 1dd70cb
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/frontend/sphinx/conf.py b/frontend/sphinx/conf.py
@@ -229,10 +229,13 @@ def get_file_from_conf_ini(path_to_file):
 #
 html_theme_options = {
     'logo_only': True,
+#    'analytics_id': '',
+#    'analytics_anonymize_ip': False,
     'display_version': False,
     'prev_next_buttons_location': 'bottom',
     'style_external_links': False,
     'vcs_pageview_mode': '',
+#    'style_nav_header_background': 'white',
     # Toc options
     'collapse_navigation': False,
     'sticky_navigation': False,