aboutsummaryrefslogtreecommitdiff
path: root/CONTRIBUTING.md
AgeCommit message (Expand)Author
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
2020-01-31Clarify expectations for overlays in contributing guide and CI doc.Théo Zimmermann
2020-01-31[contributing guide] Clarify some subtitles.Théo Zimmermann
2020-01-17Add some more info to the maintainer doc.Théo Zimmermann
2019-12-24Update merging doc following the full move to teams.Théo Zimmermann
2019-12-13Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to INSTA...Théo Zimmermann
2019-12-13[doc] [INSTALL] Port INSTALL to markdown format.Emilio Jesus Gallego Arias
2019-12-13[fmt] [dune] Add ocamlformat configuration.Emilio Jesus Gallego Arias
2019-11-27missing "Olivier Laurent
2019-11-20Fix broken linksNikita Eshkeev
2019-08-28Merge PR #10646: Recommend assigning an issue before fixing a bug.Emilio Jesus Gallego Arias
2019-08-27Add missing entry to the contributing guide TOC.Théo Zimmermann
2019-08-09Recommend assigning an issue before fixing a bug.Théo Zimmermann
2019-07-11Refactor the part about contributing to the stdlib.Théo Zimmermann
2019-07-11More positive wording of the foreword to the contributing guide.Théo Zimmermann
2019-07-11Improve contributing guide further following reviewers' comments.Théo Zimmermann
2019-07-11Refactor and expand contributing guide.Théo Zimmermann
2019-06-06Doc for per commit compile lintGaëtan Gilbert
2019-05-31Fixed typo in CONTRIBUTING.mdJose Fernando Lopez Fernandez
2019-05-21Fixing typos - Part 1JPR
2019-02-16Add links for all mentions of Gitter and Discourse.Théo Zimmermann
2019-02-16Fix English grammar.Jason Gross
2019-02-13Mention Discourse in contributing guide.Théo Zimmermann
2019-02-13Suggest asking on Discourse or Gitter.Théo Zimmermann
2019-02-13Advertise code of conduct in contributing guide.Théo Zimmermann
2019-02-13Mention coq-community in the contributing guide.Théo Zimmermann
2019-02-13Document how to add people to the contributors team.Théo Zimmermann
2019-02-13Refresh contributing guide.Théo Zimmermann
2019-01-22Remove travisGaëtan Gilbert
2018-08-29Move mention of dev/doc/critical-bugs to CONTRIBUTINGJason Gross
2018-07-16Mention the automatic use of the rebase label.Théo Zimmermann
2018-07-16Move long label links to the bottom of CONTRIBUTING.mdThéo Zimmermann
2018-07-02Clean up documentation around beginner's guide.Siddharth Bhat
2018-06-13Markdown docs: switch from absolute to relative links.Théo Zimmermann
2018-05-26Merge PR #7285: Give advice on managing GitHub notifications in CONTRIBUTING.Maxime Dénès
2018-05-14Give advice on managing GitHub notifications in CONTRIBUTING.Théo Zimmermann
2018-05-14Update CI documentation following recent evolutions.Théo Zimmermann
2018-04-05Adapt CONTRIBUTING to recent changes in Coq.Théo Zimmermann
2018-02-24Merge PR #6543: Update headers and creditsMaxime Dénès
2018-02-21Mention the CREDITS file in CONTRIBUTING.Théo Zimmermann
2018-02-08Document configure setting up pre-commit hook in CONTRIBUTING.mdGaëtan Gilbert
2018-02-08Have the pre-commit hook also fix end-of-file nlJason Gross
2018-02-08Mention linter and pre-commit hook in CONTRIBUTING.md.Gaëtan Gilbert
2018-01-06First stab at documenting the test suite.Jasper Hugunin
2017-12-21Update README and CONTRIBUTING to mention the wiki and FAQ.Théo Zimmermann
2017-11-24Update PR filter used by RM.Maxime Dénès
2017-11-23Add PR filter used by RM to the contributing guide.Maxime Dénès
2017-10-18Fixing link to GitHub issue search, and wording.Théo Zimmermann
2017-10-18Moving to GitHub issues.Théo Zimmermann
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann