Merge remote-tracking branch 'origin/main'

This commit is contained in:
Hosted Weblate 2023-08-28 20:18:38 +02:00
commit 979cac48b4
No known key found for this signature in database
GPG Key ID: A3FAAA06E6569B4C
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",