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.

Sign up for GitHub

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

Jump to bottom

Use different label than "blocker" to merge changes from PRs #37428

Closed
1 task done
tobiasdiez opened this issue Feb 22, 2024 · 1 comment
Closed
1 task done

Use different label than "blocker" to merge changes from PRs #37428

tobiasdiez opened this issue Feb 22, 2024 · 1 comment
Labels
c: scripts t: enhancement
Milestone
sage-10.4

Comments

@tobiasdiez
Copy link
Contributor

Problem Description

Currently there are 9 PRs marked as blocker, but only one of them fixes a bug in the ci and would need to be applied to other PRs. This may lead to other PRs breaking for no reason (eg #36524 is broken because of one of these blocker PRs).

Proposed Solution

Use a different label than "p1: blocker".

Alternatives Considered

No idea, open for suggestions.

Additional Information

No response

Is there an existing issue for this?

  • I have searched the existing issues for a bug report that matches the one I want to file, without success.
This was referenced Feb 22, 2024
Open
Merged
Merged
Merged
Merged
Merged
@mkoeppe
Copy link
Contributor

mkoeppe commented Aug 5, 2024

This was done in #37950.

@mkoeppe mkoeppe closed this as completed Aug 5, 2024
@mkoeppe mkoeppe added this to the sage-10.4 milestone Aug 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
c: scripts t: enhancement
Projects
None yet
Milestone
sage-10.4
Development

No branches or pull requests
2 participants
@tobiasdiez @mkoeppe