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

Update project-stable-mir.toml #1288

Closed
wants to merge 1 commit into from

Conversation

celinval
Copy link
Contributor

Bors still doesn't seem to work in our repository, and it seems that we can't merge things manually any more.

Is there any other step we need to take to enable bors?

@Kobzol
Copy link
Contributor

Kobzol commented Jan 23, 2024

Bors (homu) has to be configured manually at the moment (https://github.com/rust-lang/homu?tab=readme-ov-file#how-to-configure). CC @Mark-Simulacrum, I'm not actually sure how to do it.

Btw, isn't bors a bit overkill for this repo? 😅

@celinval
Copy link
Contributor Author

@Kobzol I have been wondering the same thing. We initially thought it would be the easiest way to collaborate to our tests by using the same workflow as the Rust repo, but enabling bors has been more challenging than we anticipated. @oli-obk do you think we should just provide write access to maintainers and give up on bors?

@oli-obk
Copy link
Contributor

oli-obk commented Jan 24, 2024

Yea, just merging stuff seems fine. We can use GitHub actions without bors for per PR CI and resolve rare merge issues manually

@Kobzol
Copy link
Contributor

Kobzol commented Jan 24, 2024

#1297

@celinval
Copy link
Contributor Author

The one thing I want to call out is that we currently cannot merge things to our main branch anymore. I have this PR open: rust-lang/project-stable-mir#60. I am a maintainer of this project, but I cannot merge it. I see the following message instead:

The base branch restricts merging to authorized users. Learn more about protected branches.

You’re not authorized to merge this pull request.

I was able to merge it before, see rust-lang/project-stable-mir#55 for the last PR that was merged.

@Kobzol
Copy link
Contributor

Kobzol commented Jan 24, 2024

#1297 should resolve that issue.

@celinval
Copy link
Contributor Author

OK... we used to be able to merge despite that line, but let's give it a shot. Thanks!

@celinval
Copy link
Contributor Author

We'll use regular GitHub process for this repo for now on. Thank you @Kobzol!

@Kobzol
Copy link
Contributor

Kobzol commented Jan 26, 2024

No problem.

@Kobzol Kobzol closed this Jan 26, 2024
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.

3 participants