Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

mergify configuration #871

Merged
merged 15 commits into from Apr 3, 2019
Merged

mergify configuration #871

Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
3af84a1
mergify configuration
cipher1024 Apr 1, 2019
0ba9304
Update .mergify.yml
ChrisHughes24 Apr 2, 2019
20af293
Update .mergify.yml
ChrisHughes24 Apr 2, 2019
24c6769
Update .mergify.yml
cipher1024 Apr 2, 2019
cb5b8e6
Update .mergify.yml
cipher1024 Apr 2, 2019
34187fb
Update .mergify.yml
jcommelin Apr 2, 2019
87736db
Update .mergify.yml
jcommelin Apr 2, 2019
b66d30e
Update .mergify.yml
jcommelin Apr 2, 2019
6db5c70
Update .mergify.yml
jcommelin Apr 2, 2019
9931136
Update .mergify.yml
jcommelin Apr 2, 2019
f922c2f
.mergify.yml [skip ci]
cipher1024 Apr 2, 2019
54efea7
Apply suggestions from code review [skip ci]
ChrisHughes24 Apr 2, 2019
8303dc0
Update .mergify.yml
jcommelin Apr 2, 2019
fd48a50
Try to fix the mergify badge
jcommelin Apr 2, 2019
d3c44f8
make 7 rules for 7 maintainers
jcommelin Apr 3, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
21 changes: 21 additions & 0 deletions .mergify.yml
View file
Open in desktop
@@ -0,0 +1,21 @@
pull_request_rules:
- name: automatic merge on CI success and review
conditions:
- status-success=continuous-integration/travis-ci/pr
- "#changes-requested-reviews-by=0"
cipher1024 marked this conversation as resolved.
Show resolved Hide resolved
- base=master
- label=ready-to-merge
actions:
delete_head_branch: {}
merge:
method: squash
cipher1024 marked this conversation as resolved.
Show resolved Hide resolved
strict: smart
strict_method: merge
cipher1024 marked this conversation as resolved.
Show resolved Hide resolved
- name: remove outdated reviews
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand this. Why would you remove the ready to merge label if there are two approving reviews and the build passed?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's only when someone commits to the branch. Just to make sure we look at the whole set of changes before approving a PR

conditions:
- base=master
actions:
dismiss_reviews:
approved: True
label:
remove: ['ready-to-merge']
1 change: 1 addition & 0 deletions README.md
View file
Open in desktop
@@ -1,6 +1,7 @@
# mathlib

[![Build Status](https://travis-ci.org/leanprover-community/mathlib.svg?branch=master)](https://travis-ci.org/leanprover-community/mathlib)
[![Mergify Status][mergify-status]][mergify]

## Lean standard library

Expand Down