Merge pull request #105 from comit-network/delete-merged-branch

Add Mergify rule to delete merged branch and bors+
This commit is contained in:
Franck Royer 2020-12-22 14:02:31 +11:00 committed by GitHub
commit b05a96d49b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

23
.mergify.yml Normal file
View File

@ -0,0 +1,23 @@
pull_request_rules:
- name: instruct bors to merge PRs with passing tests and 2 approvals
conditions:
- "#approved-reviews-by>=2"
- "#changes-requested-reviews-by=0"
- "status-success=static_analysis"
- "-status-failure~=^build"
- -conflict
- label!=work-in-progress
- label!=blocked
- label!=no-mergify
- head~=^(?!release.*).*$
- base=dev
actions:
comment:
message: "bors r+"
- name: Delete branch if the pull request is merged
conditions:
- merged
- head~=^(?!release.*).*$
actions:
delete_head_branch:
force: false