Merge pull request #12514 from 0xc0170/fix_mergify_skip

mergify: add "mergify skip" label
pull/12520/head
Martin Kojtal 2020-02-26 15:39:30 +00:00 committed by GitHub
commit a8fe8310b9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 0 deletions

View File

@ -39,6 +39,7 @@ pull_request_rules:
conditions:
# Travis failing
- status-failure~=continuous-integration/travis-ci/pr
- "label!=mergify skip"
actions:
label:
add: ['needs: work']
@ -49,6 +50,7 @@ pull_request_rules:
conditions:
# Jenkins CI failing
- status-failure~=continuous-integration/jenkins/pr-head
- "label!=mergify skip"
actions:
label:
add: ['needs: work']
@ -59,6 +61,7 @@ pull_request_rules:
conditions:
# Jenkins CI failing - any of the pipeline
- status-failure~=^jenkins-ci
- "label!=mergify skip"
actions:
label:
add: ['needs: work']
@ -120,6 +123,7 @@ pull_request_rules:
conditions:
# Labels
- "label!=do not merge"
- "label!=mergify skip"
- "label=needs: CI"
# Reviewers