Skip to content

Add workflow to prevent PR's against stable#4373

Open
d-torrance wants to merge 1 commit into
Macaulay2:developmentfrom
d-torrance:stable-pr
Open

Add workflow to prevent PR's against stable#4373
d-torrance wants to merge 1 commit into
Macaulay2:developmentfrom
d-torrance:stable-pr

Conversation

@d-torrance
Copy link
Copy Markdown
Member

@d-torrance d-torrance commented May 26, 2026

To hopefully keep us (well, me) from doing things like merging #4287 into the wrong branch again....

Opening this against stable for now to test it out. (Edit: It worked!)

AI Disclosure

Claude wrote pretty much everything

@d-torrance d-torrance changed the base branch from stable to development May 26, 2026 21:19
@mahrud
Copy link
Copy Markdown
Member

mahrud commented May 27, 2026

Wouldn't this fail on #4297?

@d-torrance
Copy link
Copy Markdown
Member Author

That's targetting development right now, so it's not a problem. (There's a chance I merge it into stable instead, e.g., if something gets merged into development at the last minute that doesn't make it into the release, which happened last time. But I think I usually merge into development first and then just fast-forward stable.)

Plus it doesn't actually prevent merging into stable -- it just serves as a big warning not to. "Oh no! The builds failed! Oh... look at the branch..."

@mahrud
Copy link
Copy Markdown
Member

mahrud commented May 27, 2026

it just serves as a big warning not to. "Oh no! The builds failed! Oh... look at the branch..."

Unless it was a [ci skip] pull request, such as e4efd1a?

@d-torrance d-torrance added Infrastructure GitHub workflows, etc. and removed github workflows labels May 27, 2026
@d-torrance
Copy link
Copy Markdown
Member Author

D'oh -- yeah lol

@mahrud
Copy link
Copy Markdown
Member

mahrud commented May 27, 2026

I mean, it's fine as a protection against almost everyone else's PRs, even if it wouldn't have prevented the merge today.

I would be very interested in a merge-bot like the one that homebrew taps use :)

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

Labels

Infrastructure GitHub workflows, etc.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants