It may not be ideal, but would it be possible to change the documentation builds to only occur periodically?
I noticed that the doc builds take roughly ~13 minutes, and if they run on each PR merge that will add up quickly. GitHub actions appears to allow scheduled actions: https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule We could trigger documentation build maybe once a week? I'm not sure what the typical number of merged PRs are per week, but if it were around 50, that's 650 minutes per week down to only 13. The downsides to this would be: a) A delay in the documentation being published b) Documentation changes that break the build are not caught early From my minimal experience with Sphinx I think it might be possible to circumvent issue b) by performing a less time intensive doc check for syntax issues in the RST files. Then once a week perform the actual build and deployment? I think this would be an easy start to implement, although I acknowledge this particular workflow is not the main source of time consumption (the Build workflow is much larger). Matteo
signature.asc
Description: PGP signature
