diff options
| -rw-r--r-- | CONTRIBUTING.md | 2 | ||||
| -rwxr-xr-x | dev/tools/check-eof-newline.sh | 22 | ||||
| -rwxr-xr-x | dev/tools/pre-commit | 11 |
3 files changed, 33 insertions, 2 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. diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh index 9e4c8661d..c5a654e21 100755 --- a/dev/tools/check-eof-newline.sh +++ b/dev/tools/check-eof-newline.sh @@ -1,12 +1,32 @@ #!/usr/bin/env bash +# Usage: check-eof-newline.sh [--fix] FILES... +# Detect missing end of file newlines for FILES. +# Files are skipped if untracked by git and depending on gitattributes. +# With --fix, automatically append a newline. +# Exit status: 1 if any file had a missing newline, 0 otherwise +# (regardless of --fix). + +FIX= +if [ "$1" = --fix ]; +then + FIX=1 + shift +fi + CODE=0 for f in "$@"; do if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \ git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \ [ -n "$(tail -c 1 "$f")" ] then - echo "No newline at end of file $f!" + if [ -n "$FIX" ]; + then + echo >> "$f" + echo "Newline appended to file $f!" + else + echo "No newline at end of file $f!" + fi CODE=1 fi done diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 59cc84856..0cd0a0b70 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -5,6 +5,17 @@ set -e +CODE=0 +git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix || CODE=1 + +if [ $CODE -ne 0 ] +then + 1>&2 echo "Some files had newline errors; they have been fixed in the working tree." + 1>&2 echo "Make sure to add them before committing." + 1>&2 echo "This may fix itself if you were using git commit -a, and you try again." + exit 1 +fi + if git diff-index --check --cached HEAD >/dev/null 2>&1 ; then : |