Prevent merging if PR marked DO NOT MERGE

pull/18319/head
Vijay Pai 6 years ago committed by GitHub
parent c5311260fd
commit 9f9c03d0f5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 6
      .github/mergeable.yml

@ -1,7 +1,11 @@
mergeable:
pull_requests:
label:
or:
and:
- must_exclude:
regex: '^disposition/DO NOT MERGE'
message: 'Pull request marked not mergeable'
- or:
- and:
- must_include:
regex: 'release notes: yes'

Loading…
Cancel
Save