Add Mergify rule to delete merged branch and bors+

pull/105/head
Franck Royer 3 years ago
parent 7d3b2faedd
commit a1c3e1fcbb
No known key found for this signature in database
GPG Key ID: A82ED75A8DFC50A4

@ -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
Loading…
Cancel
Save