aboutsummaryrefslogtreecommitdiff
path: root/CONTRIBUTING.md
AgeCommit message (Expand)Author
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
2017-08-29Fix link to debugging file.Théo Zimmermann
2017-08-18Don't belittle the size of the SE communityTej Chajed
2017-08-18Don't mention coq-club at allTej Chajed
2017-08-18Advise contributors to use SE over coq-clubTej Chajed
2017-08-15Never mind, don't mention coqdevTej Chajed
2017-08-15Mention coqdev@Tej Chajed
2017-08-12Also mention Stack ExchangeTej Chajed
2017-08-12Add some things Jason mentionedTej Chajed
2017-08-12Expand PR process explanationTej Chajed
2017-08-12Link to the existing list of tutorialsTej Chajed
2017-08-10Simplify a bit of wordingTej Chajed
2017-08-10Describe pull requests a bit more preciselyTej Chajed
2017-08-10Some more tweaks to contributing guideTej Chajed
2017-08-10Amendments to contributing docTej Chajed
2017-08-10Add a set of contributing guidelinesTej Chajed
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:54:57 +0000