Merge pull request #7508 from dhalbert/fix-rtd

Fix broken RTD builds
This commit is contained in:
MicroDev 2023-01-30 13:27:30 +05:30 committed by GitHub
commit 72981cf2ab
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -14,7 +14,7 @@ build:
python: "3" python: "3"
jobs: jobs:
post_install: post_install:
- python tools/ci_fetch_deps.py docs HEAD - python tools/ci_fetch_deps.py build-doc
formats: formats:
- pdf - pdf