From 7a4049b683499a80df92f0c6181af259f28a0a95 Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Wed, 3 Sep 2025 19:28:17 -0400 Subject: [PATCH] Fix docs HTML format from last commit --- docs/guide/conf.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/docs/guide/conf.py b/docs/guide/conf.py index 075e91e9a..33ce181ac 100644 --- a/docs/guide/conf.py +++ b/docs/guide/conf.py @@ -110,6 +110,9 @@ html_domain_indices = False html_logo = "../_static/verilator_192_150_min.png" html_theme = 'sphinx_rtd_theme' +# Despite a 'WARNING: Calling get_html_theme_path is deprecated' +# the HTML output is different without this line +html_theme_path = [sphinx_rtd_theme.get_html_theme_path()] html_theme_options = { 'logo_only': True,