aboutsummaryrefslogtreecommitdiffhomepage
path: root/CONTRIBUTING.md
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-01-18 16:42:44 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-08 17:15:22 +0100
commit04a3fa7eac845039b0b1a11d1a5958486f183a4d (patch)
tree2805b39efa169b9d8df59acb0959a7d0b2443e28 /CONTRIBUTING.md
parent8ab30d25b5ffc6a56e9ca41f446504bba4a726ad (diff)
Document configure setting up pre-commit hook in CONTRIBUTING.md
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 0faf2cdfc..74a138f14 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -32,7 +32,7 @@ If your pull request fixes a bug, please consider adding a regression test as we
Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
-Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). You can ensure that your commits do not introduce errors by adding the [`dev/tools/pre-commit`](/dev/tools/pre-commit) script to your `.git/hooks/` directory.
+Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.