Skip to content

test: on an old master, the PR summary suggests to merge master#21699

Closed
adomani wants to merge 2 commits intomasterfrom
test/please_merge_mastr
Closed

test: on an old master, the PR summary suggests to merge master#21699
adomani wants to merge 2 commits intomasterfrom
test/please_merge_mastr

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented Feb 11, 2025

Testing the name of the file produced when there is a PR_summary script mismatch.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

please_merge_master.md

@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 11, 2025

Setting myself up for testing the bors d- action.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 11, 2025

✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 11, 2025
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 11, 2025

Let's see if the delegated label gets removed.

bors d-

EDIT: #21676, the PR with the fix, has not been merged yet...

@adomani adomani removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 11, 2025
@adomani adomani changed the title line break test: on an old master, the PR summary suggests to merge master Feb 11, 2025
@adomani adomani added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. labels Feb 11, 2025
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 11, 2025

bors d-

@ghost ghost removed ready-to-merge This PR has been sent to bors. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). labels Feb 11, 2025
@adomani adomani added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. labels Feb 11, 2025
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 11, 2025

bors r-

@ghost ghost removed ready-to-merge This PR has been sent to bors. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). labels Feb 11, 2025
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 11, 2025

This PR was intended to show the please_merge_master.md message. I also hijacked it to test the bors r-/bors d- removal of the appropriate labels.

It can be closed now.

@adomani adomani closed this Feb 11, 2025
@YaelDillies YaelDillies deleted the test/please_merge_mastr branch August 17, 2025 11:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant