aboutsummaryrefslogtreecommitdiff
path: root/.github
AgeCommit message (Collapse)Author
2018-03-29Remove dev/doc/changes.md from files with a code owner.Théo Zimmermann
Like CHANGES, and the test-suite folder, this file receives too many updates to have a code owner. It is the job of the reviewer of the PR to review changes to these files as well.
2018-03-26Add Michael Soegtrop as a code owner for Windows build scripts.Théo Zimmermann
2018-03-26Use Pierre Corbineau GitHub nickname in CODEOWNERS.Théo Zimmermann
2018-03-23Merge PR #7046: Switch maintainers for documentationThéo Zimmermann
2018-03-22Owners for developer toolsMaxime Dénès
2018-03-22Switch maintainers for documentationMaxime Dénès
Guillaume and I agreed to switch, as the new Sphinx infrastructure changes this component significantly.
2018-03-21Switching owners for `META.coq`Maxime Dénès
2018-03-21Fix appveyor entry in CODEOWNERS.Maxime Dénès
2018-03-21Refine a bit the decentralized merging process.Maxime Dénès
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.
2018-03-20Update CODEOWNERSEnrico
2018-03-20Add CODEOWNERSMaxime Dénès
See https://help.github.com/articles/about-codeowners/ for documentation.
2018-01-05[PR template] Remove the relative link.Théo Zimmermann
Was actually pointing to https://github.com/CHANGES.
2017-12-24Create pull request template.Théo Zimmermann
2017-11-13Move contributing files to .github/ sub-directory.Théo Zimmermann
The overall goal is to reduce the number of files at the root of the repository.