You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Mar 24, 2022. It is now read-only.
One important limitation I just noticed: the CircleCI build only runs on the commit of a PR's branch (what GH Actions labels the push), it does not automatically run on the merge commit (what Actions calls pull_request).
This raises the possibility that if a PR is not up to date with master, all of the CI might go green for a PR, we'll press the big green button, and the resulting merge commit into master will fail. The silver lining is that it will fail, since CircleCI runs on all commits by default.
This is also another case where using bors would help, since bors creates staging commits that are never behind master. Maybe it's time to set up bors for this repo?
I have only lightly interacted with bors when submitting patches to rust-lang projects. Let's investigate further to see whether we'd like to enable bors for this repo.