diff options
-rw-r--r-- | Documentation/conf.py | 3 | ||||
-rw-r--r-- | Documentation/sphinx-static/custom.css | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/Documentation/conf.py b/Documentation/conf.py index 6ab47833ab6c..c715610d6297 100644 --- a/Documentation/conf.py +++ b/Documentation/conf.py @@ -316,9 +316,10 @@ if major <= 1 and minor < 8: if html_theme == 'alabaster': html_theme_options = { 'description': get_cline_version(), - 'font_size': '10pt', 'page_width': '65em', 'sidebar_width': '15em', + 'font_size': 'inherit', + 'font_family': 'serif', } sys.stderr.write("Using %s theme\n" % html_theme) diff --git a/Documentation/sphinx-static/custom.css b/Documentation/sphinx-static/custom.css index 9b36f7abd24f..45a624fdcf2c 100644 --- a/Documentation/sphinx-static/custom.css +++ b/Documentation/sphinx-static/custom.css @@ -11,6 +11,7 @@ div.body h3 { font-size: 130%; } /* Tighten up the layout slightly */ div.body { padding: 0 15px 0 10px; } div.sphinxsidebarwrapper { padding: 1em 0.4em; } +div.sphinxsidebar { font-size: inherit; } /* Tweak document margins and don't force width */ div.document { margin: 20px 10px 0 10px; |