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

ci: prevent merge of PRs with do-not-merge label #1006

Merged
merged 1 commit into from
Nov 18, 2024

Conversation

burgerdev
Copy link
Contributor

No description provided.

@burgerdev burgerdev added no changelog PRs not listed in the release notes do not merge This shouldn't be merged at this point labels Nov 17, 2024
@burgerdev burgerdev removed the do not merge This shouldn't be merged at this point label Nov 17, 2024
@burgerdev
Copy link
Contributor Author

@burgerdev burgerdev force-pushed the burgerdev/do-not-merge branch from 88a6867 to 18923b5 Compare November 18, 2024 07:11
@burgerdev burgerdev added the do not merge This shouldn't be merged at this point label Nov 18, 2024
@burgerdev burgerdev force-pushed the burgerdev/do-not-merge branch 2 times, most recently from 72e9dba to b363d14 Compare November 18, 2024 07:17
@burgerdev burgerdev removed the do not merge This shouldn't be merged at this point label Nov 18, 2024
@burgerdev
Copy link
Contributor Author

I'm not going to rerun the e2e tests unless asked to, the PR should be fine now.

@burgerdev burgerdev requested a review from katexochen November 18, 2024 10:41
Copy link
Member

@katexochen katexochen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

actually, I don't think we even need to write to summary, annotation is already shown there anyway:
image

But I'm also fine to merge like this.

@burgerdev burgerdev force-pushed the burgerdev/do-not-merge branch from b363d14 to 3538f8b Compare November 18, 2024 11:41
@burgerdev burgerdev added do not merge This shouldn't be merged at this point and removed do not merge This shouldn't be merged at this point labels Nov 18, 2024
@burgerdev
Copy link
Contributor Author

Thanks, we don't need the summary then.

@burgerdev burgerdev force-pushed the burgerdev/do-not-merge branch from 3538f8b to 207fbc8 Compare November 18, 2024 11:43
@burgerdev burgerdev merged commit a02940a into main Nov 18, 2024
10 checks passed
@burgerdev burgerdev deleted the burgerdev/do-not-merge branch November 18, 2024 13:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
no changelog PRs not listed in the release notes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants