There is no use in the documentation-generation pipeline being run with every commit. It should be sufficient to run it once before merging.
\rfc @laurens @pdlmora @tara @gislars