-
Notifications
You must be signed in to change notification settings - Fork 119
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: fix PR title ci job concurrency #1451
base: main
Are you sure you want to change the base?
Conversation
I was thinking to use branch names first, but what if both tony and david issue a PR from their forks' main? |
Interestingly, the documentation indicates that I can't find the documentation for |
Ah, I see that for the linked PR where we had this issue, EDIT: or the documentation is just wrong? |
Bad docs. I think they meant to say "for a pull request merge event," or something alike. It's clearly the base branch for outstanding pull requests in the context of the I guess Or, rather, target is reasonable, but plain PR event is magical, because if the base branch has moved on, GitHub will make a "fake merge" (what you'd get if you merged the PR right now) to run the action against, and if there's no clean fake merge, it'd run against "fake merge against base" or something like that. Convoluted. |
A penny for anyone's review? |
https://matrix.to/#/!eNCNzcteYUDDYpStsu:ubuntu.com/$PjGy1bizJkNGgu-A629wckDFKPzEQ5BKXIkmlE8sUyg?via=ubuntu.com&via=matrix.org