diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-09 13:11:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-09 13:11:49 +0200 |
| commit | 55f59acbd9cdec6188613edc29e49d5f5a4f6d98 (patch) | |
| tree | 3ef86ecf1f9300fbf7e7260a2a51e868a78cf2ce /plugins/ltac/tacinterp.ml | |
| parent | a44b4be1bf8b96e941216cd10cfb5981a825c3fa (diff) | |
Introduce a team of code owners for the CI system.
This means that all the members of the team will receive
a review request for PRs on the CI, but only one of them
will need to approve the PR, and this will remove the
review request for the others.
Currently the team contains Emilio and Gaetan, the two
former code owners of these files. It makes sense to start
experimenting on this component since they had already
decided to make their role symmetric.
Updating the list of maintainers can be done by updating
the list members, and without changing the CODEOWNER file.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
0 files changed, 0 insertions, 0 deletions