diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/lint-commits.sh | 31 |
1 files changed, 25 insertions, 6 deletions
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index 96c92e3162..539bb5f1f9 100755 --- a/dev/lint-commits.sh +++ b/dev/lint-commits.sh @@ -19,21 +19,40 @@ fi BASE_COMMIT="$1" HEAD_COMMIT="$2" -bad=() +bad_ws=() +bad_compile=() while IFS= read -r commit; do echo Checking "$commit" # git diff --check # uses .gitattributes to know what to check if ! git diff --check "${commit}^" "$commit"; - then - bad+=("$commit") + then bad_ws+=("$commit") + fi + + if ! make -f Makefile.dune check + then bad_compile+=("$commit") fi done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --) -if [ "${#bad[@]}" != 0 ] +# report errors + +CODE=0 + +if [ "${#bad_ws[@]}" != 0 ] then >&2 echo "Whitespace errors!" - >&2 echo "In commits ${bad[*]}" + >&2 echo "In commits ${bad_ws[*]}" >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." - exit 1 + >&2 echo + CODE=1 fi + +if [ "${#bad_compile[@]}" != 0 ] +then + >&2 echo "Compilation errors!" + >&2 echo "In commits ${bad_compile[*]}" + >&2 echo + CODE=1 +fi + +exit $CODE |