-
Notifications
You must be signed in to change notification settings - Fork 296
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
Conversation
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? 😅 |
@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? |
Yea, just merging stuff seems fine. We can use GitHub actions without bors for per PR CI and resolve rare merge issues manually |
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:
I was able to merge it before, see rust-lang/project-stable-mir#55 for the last PR that was merged. |
#1297 should resolve that issue. |
OK... we used to be able to merge despite that line, but let's give it a shot. Thanks! |
We'll use regular GitHub process for this repo for now on. Thank you @Kobzol! |
No problem. |
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?