Skip to content
This repository was archived by the owner on Jan 15, 2026. It is now read-only.

set up auto-labeling for Miri#219

Closed
RalfJung wants to merge 1 commit intorust-lang:masterfrom
RalfJung:miri-labels
Closed

set up auto-labeling for Miri#219
RalfJung wants to merge 1 commit intorust-lang:masterfrom
RalfJung:miri-labels

Conversation

@RalfJung
Copy link
Member

No description provided.

@RalfJung
Copy link
Member Author

Miri isn't using homu any more so this is redundant.

@RalfJung RalfJung closed this Oct 22, 2024
@RalfJung
Copy link
Member Author

@rust-lang/infra the entire "Miri" section can be removed now, I assume?

I'll probably better let you handle that.

@Kobzol
Copy link
Member

Kobzol commented Oct 22, 2024

The last time I tried to remove a repo from https://bors.rust-lang.org/, it completely broke homu. So I'd probably just wait until we get rid of homu completely and avoid making changes to it. It shouldn't cause issues that homu still thinks that he's in charge.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants