Linter: check that files end with newlines.

We use git check-attr to look at the same files as git diff --check.

1 files changed, 28 insertions, 0 deletions

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
new file mode 100755
index 000000000..ecf7880e2
--- /dev/null
+++ b/dev/lint-repository.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+
+# A script to check prettyness over the repository.
+
+# lint-commits.sh seeks to prevent the worsening of already present
+# problems, such as tab indentation in ml files. lint-repository.sh
+# seeks to prevent the (re-)introduction of solved problems, such as
+# newlines at the end of .v files.
+
+CODE=0
+
+if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ];
+then
+    # Some problems are too widespread to fix in one commit, but we
+    # can still check that they don't worsen.
+    CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
+    PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
+    MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
+    dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1
+fi
+
+# Check that the files with 'whitespace' gitattribute end in a newline.
+# xargs exit status is 123 if any file failed the test
+find . "(" -path ./.git -prune ")" -type f \
+-o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \
+-print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1
+
+exit $CODE