mirror of https://github.com/ARMmbed/mbed-os.git
Merge pull request #15127 from 0xc0170/fix-mergify-closed-prs
mergify: fix issue with labels when PR is closedpull/15079/head^2
commit
9dd6fb4495
|
@ -58,6 +58,7 @@ pull_request_rules:
|
||||||
# Jenkins CI failing
|
# Jenkins CI failing
|
||||||
- check-failure~=continuous-integration/jenkins/pr-head
|
- check-failure~=continuous-integration/jenkins/pr-head
|
||||||
- "label!=mergify skip"
|
- "label!=mergify skip"
|
||||||
|
- -closed
|
||||||
actions:
|
actions:
|
||||||
label:
|
label:
|
||||||
add: ['needs: work']
|
add: ['needs: work']
|
||||||
|
|
Loading…
Reference in New Issue