aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
Commit message (Collapse)AuthorAge
* Add myself as the primary maintainer of the warnings systemGravatar Maxime Dénès2018-04-11
|
* Remove dev/doc/changes.md from files with a code owner.Gravatar Théo Zimmermann2018-03-29
| | | | | | 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.
* Add Michael Soegtrop as a code owner for Windows build scripts.Gravatar Théo Zimmermann2018-03-26
|
* Use Pierre Corbineau GitHub nickname in CODEOWNERS.Gravatar Théo Zimmermann2018-03-26
|
* Merge PR #7046: Switch maintainers for documentationGravatar Théo Zimmermann2018-03-23
|\
* | Owners for developer toolsGravatar Maxime Dénès2018-03-22
| |
| * Switch maintainers for documentationGravatar Maxime Dénès2018-03-22
|/ | | | | Guillaume and I agreed to switch, as the new Sphinx infrastructure changes this component significantly.
* Switching owners for `META.coq`Gravatar Maxime Dénès2018-03-21
|
* Fix appveyor entry in CODEOWNERS.Gravatar Maxime Dénès2018-03-21
|
* Refine a bit the decentralized merging process.Gravatar Maxime Dénès2018-03-21
| | | | | | | | | | | | 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.
* Update CODEOWNERSGravatar Enrico2018-03-20
|
* Add CODEOWNERSGravatar Maxime Dénès2018-03-20
| | | | | See https://help.github.com/articles/about-codeowners/ for documentation.
* [PR template] Remove the relative link.Gravatar Théo Zimmermann2018-01-05
| | | | Was actually pointing to https://github.com/CHANGES.
* Create pull request template.Gravatar Théo Zimmermann2017-12-24
|
* Move contributing files to .github/ sub-directory.Gravatar Théo Zimmermann2017-11-13
The overall goal is to reduce the number of files at the root of the repository.