diff options
author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2020-06-13 00:50:07 +0200 |
---|---|---|
committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2020-06-20 23:40:46 +0200 |
commit | c59158c8f96750609ec7e67281cdfb2881d8235d (patch) | |
tree | 133df503537dfaac034d8faf9e69a1dc133170b9 | |
parent | 8451604a75f8bbaaa65a57819134f2dea5a4c29d (diff) | |
download | sparse-c59158c8f96750609ec7e67281cdfb2881d8235d.tar.gz |
doc: switch to the sphinx_rtd theme
The generated documentation used Sphinx's classic/default theme
but the one from readthedocs ('rtd', the same as used for the kernel)
looks nicer, especially in the sidebar, and is not as large.
So, for now, switch to the 'rtd' theme.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
-rw-r--r-- | Documentation/conf.py | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Documentation/conf.py b/Documentation/conf.py index bd2532f7..89ba3d78 100644 --- a/Documentation/conf.py +++ b/Documentation/conf.py @@ -100,7 +100,14 @@ cdoc_srcdir = '..' # The theme to use for HTML and HTML Help pages. See the documentation for # a list of builtin themes. # -html_theme = 'classic' +try: + html_theme = 'sphinx_rtd_theme' + import sphinx_rtd_theme + html_theme_path = [sphinx_rtd_theme.get_html_theme_path()] +except: + sys.stderr.write("Warning: theme '%s' not found\n" % html_theme) + html_theme = 'classic' + # html_theme_options = {} # Add any paths that contain custom static files (such as style sheets) here, |