diff options
| author | Maxime Dénès | 2018-03-21 13:53:20 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-21 16:11:01 +0100 |
| commit | e554ad813af2e51606284cc628202919ba89d34c (patch) | |
| tree | 9362c11cd30af5ae34f2662d1af24a63da4e1acf /kernel/type_errors.ml | |
| parent | 17c94dca5fe2fc19137b9cac923d51e8eb818041 (diff) | |
Refine a bit the decentralized merging process.
We make GitHub assign only principal maintainers as reviewers. This
reduces the level of noise (PRs with 10 code owners), and makes it easy
for the assignee to check if all reviews have been completed (all
reviewers in the list have to approve the PR, which was not the case
before if two reviewers were assigned for the same component).
This change means that when a principal maintainer submits a patch
touching the component they own, they should ask a review from the
secondary maintainer.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions
