aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-21 13:53:20 +0100
committerMaxime Dénès2018-03-21 16:11:01 +0100
commite554ad813af2e51606284cc628202919ba89d34c (patch)
tree9362c11cd30af5ae34f2662d1af24a63da4e1acf /kernel/nativelambda.ml
parent17c94dca5fe2fc19137b9cac923d51e8eb818041 (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/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions