aboutsummaryrefslogtreecommitdiff
path: root/CONTRIBUTING.md
AgeCommit message (Collapse)Author
2021-03-10Fix a hyperlink in CONTRIBUTING.mdKazuhiko Sakaguchi
2020-07-30Merging is now possible with coqbot.Théo Zimmermann
This is proposed as an alternative to the merge script, in particular for maintainers without a GPG key.
2020-07-09Fix typo in contributing guide.Théo Zimmermann
Notice by Jim Fehrle.
2020-05-20Adapt the documentation to the move from Gitter to Zulip.Théo Zimmermann
2020-05-13Clarify the assignee's role in removing the overlay informationAnton Trunov
2020-05-13Clarify the documentation for merging PRs with overlaysAnton Trunov
2020-04-21Merge PR #12113: Contributing guide improvementsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-17Adapt linter documentation to the recent improvements of the pre-commit hook.Théo Zimmermann
2020-04-17More documentation on draft PRs.Théo Zimmermann
2020-04-17Contributing guide: turn some sub-sections into sub-sub-sections.Théo Zimmermann
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-01-31Clarify expectations for overlays in contributing guide and CI doc.Théo Zimmermann
Contributors are *not* required to prepare all the patches by themselves. They can request help from project authors, who should be ready to take part in this. Also, finish replacing "development" by the more appropriate word "project".
2020-01-31[contributing guide] Clarify some subtitles.Théo Zimmermann
2020-01-17Add some more info to the maintainer doc.Théo Zimmermann
- What is consensus - How to join / leave Following suggestions from Vincent Semeriva and Maxime Dénès.
2019-12-24Update merging doc following the full move to teams.Théo Zimmermann
Integrate merging doc in the main contributing document.
2019-12-13Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to ↵Théo Zimmermann
INSTALL.md Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: jfehrle
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
For now we don't enable it in any source file, neither on dune files. `lint-repository` has been updated so it will check `dune build @fmt` returns 0.
2019-11-27missing "Olivier Laurent
2019-11-20Fix broken linksNikita Eshkeev
This patch fixes broken links in the CONTRIBUTING.md document
2019-08-28Merge PR #10646: Recommend assigning an issue before fixing a bug.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-27Add missing entry to the contributing guide TOC.Théo Zimmermann
And add links to UI in the browser.
2019-08-09Recommend assigning an issue before fixing a bug.Théo Zimmermann
Contributors with write-access can now assign people who commented an issue: https://github.blog/changelog/2019-06-25-assign-issues-to-issue-commenters/
2019-07-11Refactor the part about contributing to the stdlib.Théo Zimmermann
- Remove reference to the age of the stdlib - Remove reference to stdlib2 until it accepts contributions - Merge two paragraphs together - Minor wording improvements
2019-07-11More positive wording of the foreword to the contributing guide.Théo Zimmermann
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2019-07-11Improve contributing guide further following reviewers' comments.Théo Zimmermann
Thanks to the reviewers: Jim Fehrle, Emilio Gallego, Gaëtan Gilbert, Enrico Tassi.
2019-07-11Refactor and expand contributing guide.Théo Zimmermann
This is almost a full rewrite of the contributing guide. The goal was to have a more structured, and more exhaustive guide, where all our processes are documented, and from which all the useful documentation is linked to. The document lists contribution types in the order in which it is most natural to go through them: from contributions to the ecosystem, to issues, to code contributions, to taking part in the maintenance. However, it seemed important to not neglect this last part if we want to ease the onboarding of new maintainers (and not just of occasional contributors). A table of content makes it easy to go through the document (which is too long to be read from begin to end). The guide documents our processes in the way they are today, without changing anything, but this should be a good basis to make them evolve in the future. Insufficiently documented tools and processes are mentioned as such.
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
Update the part about following the development. Remove the reference to Coqdev.
2019-02-16Fix English grammar.Jason Gross
Co-Authored-By: Zimmi48 <theo.zimmermann@univ-paris-diderot.fr>
2019-02-13Mention Discourse in contributing guide.Théo Zimmermann
2019-02-13Suggest asking on Discourse or Gitter.Théo Zimmermann
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
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
The azure OSX job replaces the first travis job, and the second always fails and so is useless.
2018-08-29Move mention of dev/doc/critical-bugs to CONTRIBUTINGJason Gross
As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
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
- move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
2018-06-13Markdown docs: switch from absolute to relative links.Théo Zimmermann
We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]
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
- The testing and benchmarking labels are now distinct. - The release manager does not take care of merging anymore. - The reference manual is not written in LaTeX anymore.
2018-02-24Merge PR #6543: Update headers and creditsMaxime Dénès
2018-02-21Mention the CREDITS file in CONTRIBUTING.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:15 +0000