Merge remote-tracking branch 'origin/8.2.x' into merge-82x

This commit is contained in:
Jeff Epler 2023-08-28 08:30:30 -05:00
commit e44c2c06f4
No known key found for this signature in database
GPG Key ID: D5BF15AB975AB4DE
2 changed files with 4 additions and 13 deletions

16
conf.py
View File

@ -266,19 +266,9 @@ rst_epilog = """
# -- Options for HTML output ----------------------------------------------
# on_rtd is whether we are on readthedocs.org
on_rtd = os.environ.get('READTHEDOCS', None) == 'True'
if not on_rtd: # only import and set the theme if we're building docs locally
try:
import sphinx_rtd_theme
html_theme = 'sphinx_rtd_theme'
html_theme_path = [sphinx_rtd_theme.get_html_theme_path(), '.']
except:
html_theme = 'default'
html_theme_path = ['.']
else:
html_theme_path = ['.']
import sphinx_rtd_theme
html_theme = 'sphinx_rtd_theme'
html_theme_path = [sphinx_rtd_theme.get_html_theme_path(), '.']
# Theme options are theme-specific and customize the look and feel of a theme
# further. For a list of options available for each theme, see the

View File

@ -45,6 +45,7 @@ from shared_bindings_matrix import (
# Files that never influence board builds
IGNORE_BOARD = {
".devcontainer",
"conf.py",
"docs",
"tests",
"tools/ci_changes_per_commit.py",