aboutsummaryrefslogtreecommitdiffhomepage
path: root/CONTRIBUTING.md
diff options
context:
space:
mode:
authorGravatar Tej Chajed <tchajed@mit.edu>2017-08-10 16:25:52 +0100
committerGravatar Tej Chajed <tchajed@mit.edu>2017-08-10 16:25:52 +0100
commit82ac0208b86c8a3a913e10c81208e0716d2d4bcf (patch)
treed296f36f406d5eeebb0a52768a6d48a293e4b40b /CONTRIBUTING.md
parentde170f36c9b8e36810126fec82ff9cce2a2af2e7 (diff)
Describe pull requests a bit more precisely
Diffstat (limited to 'CONTRIBUTING.md')
-rw-r--r--CONTRIBUTING.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 983eb64a1..2aaec12a9 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -18,7 +18,7 @@ When it applies, it's extremely helpful for bug reports to include sample code,
## Pull requests
-Sometimes you are able to contribute a bug fix or improvement yourself, and pull requests are the mechanism to get these changes into Coq. Documentation for getting started with the Coq sources is located at [`dev/doc`](/dev/doc).
+If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](/dev/doc) (for example, [debugging.txt](/dev/doc/debugging.txt)).
Please make pull requests against the `master` branch.