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

mergify: fix issue with labels when PR is closed #15127

Merged
merged 1 commit into from
Oct 5, 2021
Merged

mergify: fix issue with labels when PR is closed #15127

merged 1 commit into from
Oct 5, 2021

Conversation

0xc0170
Copy link
Contributor

@0xc0170 0xc0170 commented Oct 4, 2021

Summary of changes

This fixes an issue with mergify when PR is closed (See Mergifyio/mergify#3307 for details).

Impact of changes

Migration actions required

Documentation

Pull request type 

[x] Patch update (Bug fix / Target update / Docs update / Test update / Refactor)
[] Feature update (New feature / Functionality change / New API)
[] Major update (Breaking change E.g. Return code change / API behaviour change)

Test results 

[x] No Tests required for this change (E.g docs only update)
[] Covered by existing mbed-os tests (Greentea or Unittest)
[] Tests / results supplied as part of this PR

Reviewers

@ciarmcom ciarmcom added the release-type: patch Indentifies a PR as containing just a patch label Oct 4, 2021
@ciarmcom ciarmcom requested a review from a team October 4, 2021 13:30
@ciarmcom
Copy link
Member

ciarmcom commented Oct 4, 2021

@0xc0170, thank you for your changes.
@ARMmbed/mbed-os-maintainers please review.

@mergify mergify bot added needs: CI and removed needs: review labels Oct 4, 2021
@0xc0170
Copy link
Contributor Author

0xc0170 commented Oct 5, 2021

CI started

@0xc0170 0xc0170 merged commit 9dd6fb4 into ARMmbed:master Oct 5, 2021
@0xc0170 0xc0170 deleted the fix-mergify-closed-prs branch October 5, 2021 09:33
@mergify mergify bot removed the ready for merge label Oct 5, 2021
@mbedmain mbedmain added release-version: 6.15.1 Release-pending and removed release-type: patch Indentifies a PR as containing just a patch Release-pending labels Nov 22, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@adbridge adbridge adbridge approved these changes

Assignees
No one assigned
Labels
release-version: 6.15.1
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@0xc0170 @ciarmcom @adbridge @mbedmain