blob: 95b72787fb88f330f080a1db14d1c1a9508bb86e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
#!/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}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ];
then
# skip PRs from before the linter existed
if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
then
2>&1 echo "Linting skipped: pull request older than the linter."
exit 0
fi
# 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
|
