Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix bors by updating status names to include OS #1851

Merged
merged 1 commit into from May 14, 2020

Conversation

hudson-ayers
Copy link
Contributor

@hudson-ayers hudson-ayers commented May 14, 2020

Pull Request Overview

This pull request updates the status names that Bors blocks on before merging PRs. #1625 introduced jobs which run on multiple different OSes, so Github reports job names to Bors that include the OS of the runner for that job. Bors is expecting the old names, and so eventually times out.

This PR updates the names to match the names reported by Github.

Testing Strategy

This pull request has not been tested. The easiest test would be for someone to approve this and tell bors to merge it and see if it works -- if it works its correct, if not it doesn't merge!

TODO or Help Wanted

N/A

Documentation Updated

  • No updates are required.

Formatting

  • Ran make formatall.

Copy link
Member

@ppannuto ppannuto left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors r+

Well, let's see

@bors
Copy link
Contributor

bors bot commented May 14, 2020

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

@bors bors bot merged commit cc2f0ff into tock:master May 14, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants