aboutsummaryrefslogtreecommitdiffhomepage
path: root/CONTRIBUTING.md
diff options
context:
space:
mode:
authorGravatar Jason Gross <jasongross9@gmail.com>2018-01-16 18:12:55 +0100
committerGravatar Gaƫtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-08 17:15:20 +0100
commit8ab30d25b5ffc6a56e9ca41f446504bba4a726ad (patch)
tree8936bd55cb6f1b1cd181f6bdd023b898e43f3f32 /CONTRIBUTING.md
parentd31777adb88eb5ba54f68ac7a4cb7a2a29c1fc20 (diff)
Have the pre-commit hook also fix end-of-file nl
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 0d35e52cb..0faf2cdfc 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) 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. Travis also enforces that text files end in newlines, but the script does not help with this.
+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.
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.