Description
With a constant branch name introduced in 114fe57, once the branch exists on origin
, subsequent failed builds will fail to push their changes to the constant branch, since the push is not a fast-forward of the existing dereference.
This prevents the diff for the existing PR from being updated, meaning that once a build fails attempts to fix the build are outside the PR feedback loop.
Additionally, after a failed-build-PR is merged or closed, users must remember to manually clean up the branch (e.g., by deleting it in the Github UI or by pushing a deletion with git push origin :versioned_docs_failed_build
), or else subsequent build failures will open up a new PR that points to a previous failure.
Should we add a --force
to the git push
command when opening that PR? This would cause the in-flight PR to get updated on each subsequent build failure, but the nature of a force-push could be surprising to anyone attempting to manually fix-up the PR.