aboutsummaryrefslogtreecommitdiff
path: root/.github
AgeCommit message (Expand)Author
2018-04-17Assign circleci files to @SkySkimmer, @ejgallegoGaëtan Gilbert
2018-04-11Add myself as the primary maintainer of the warnings systemMaxime Dénès
2018-03-29Remove dev/doc/changes.md from files with a code owner.Théo Zimmermann
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
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
2018-03-20Update CODEOWNERSEnrico
2018-03-20Add CODEOWNERSMaxime Dénès
2018-01-05[PR template] Remove the relative link.Théo Zimmermann
2017-12-24Create pull request template.Théo Zimmermann
2017-11-13Move contributing files to .github/ sub-directory.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:27:20 +0000