diff options
| author | Théo Zimmermann | 2019-12-15 15:41:05 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-22 21:46:50 +0100 |
| commit | c32e1c54c87231b6411d3002766972e18438fc4a (patch) | |
| tree | 9ab84e7b93cf261039cfcfa12b50445270a0791a /dev | |
| parent | df12d00bd01801088b6b8c50e51142e646053829 (diff) | |
Use code owner teams for every component.
It was decided during the Coq WG that code owner teams are more
convenient, in particular because they allow adding and removing team
members without going through a pull request. For each team, we
should aim to have at least three code owners, even if in some cases
we are going to start with less.
We also stop triggering review requests for changelog entries as was
also decided during the WG.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions