Merge pull request #8342 from jepler/merge-82x

Merge 8.2.x into main
This commit is contained in:
Scott Shawcroft 2023-08-28 11:18:33 -07:00 committed by GitHub
commit def7463c37
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 4 additions and 13 deletions

10
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 = ['.']
# 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",