Add linter.

3 files changed, 80 insertions, 0 deletions

diff --git a/.gitattributes b/.gitattributes
index 00f78b449..f2c096f2d 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,3 +1,36 @@
 .gitattributes export-ignore
 .gitignore export-ignore
 .mailmap export-ignore
+
+*.asciidoc whitespace=trailing-space,tab-in-indent
+*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent
+*.bib whitespace=trailing-space,tab-in-indent
+*.c whitespace=trailing-space,tab-in-indent
+*.css whitespace=trailing-space,tab-in-indent
+*.dtd whitespace=trailing-space,tab-in-indent
+*.el whitespace=trailing-space,tab-in-indent
+*.h whitespace=trailing-space,tab-in-indent
+*.html whitespace=trailing-space,tab-in-indent
+*.hva whitespace=trailing-space,tab-in-indent
+*.js whitespace=trailing-space,tab-in-indent
+*.json whitespace=trailing-space,tab-in-indent
+*.lang whitespace=trailing-space,tab-in-indent
+*.md whitespace=trailing-space,tab-in-indent
+*.merlin whitespace=trailing-space,tab-in-indent
+*.ml whitespace=trailing-space,tab-in-indent
+*.ml4 whitespace=trailing-space,tab-in-indent
+*.mli whitespace=trailing-space,tab-in-indent
+*.mll whitespace=trailing-space,tab-in-indent
+*.mllib whitespace=trailing-space,tab-in-indent
+*.mlp whitespace=trailing-space,tab-in-indent
+*.mlpack whitespace=trailing-space,tab-in-indent
+*.nsh whitespace=trailing-space,tab-in-indent
+*.nsi whitespace=trailing-space,tab-in-indent
+*.py whitespace=trailing-space,tab-in-indent
+*.sh whitespace=trailing-space,tab-in-indent
+*.sty whitespace=trailing-space,tab-in-indent
+*.tex whitespace=trailing-space,tab-in-indent
+*.txt whitespace=trailing-space,tab-in-indent
+*.v whitespace=trailing-space,tab-in-indent
+*.xml whitespace=trailing-space,tab-in-indent
+*.yml whitespace=trailing-space,tab-in-indent
diff --git a/.travis.yml b/.travis.yml
index 1a9f6964f..4e937b50f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -135,6 +135,21 @@ matrix:
           - avsm
           packages: *coqide-packages
 
+    - if: type = pull_request
+      env:
+      - TEST_TARGET="lint"
+      install: []
+      before_script: []
+      addons:
+      apt:
+        sources: []
+        packages: []
+      script:
+        - 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
+
     - os: osx
       osx_image: xcode8.3
       env:
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
new file mode 100755
index 000000000..eb12bc227
--- /dev/null
+++ b/dev/lint-commits.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+# A script to check prettyness for a range of commits
+
+CALLNAME="$0"
+
+function usage
+{
+    >&2 echo "usage: $CALLNAME <commit> <commit>"
+    >&2 echo "The order of commits is as given to 'git diff'"
+}
+
+if [ "$#" != 2 ];
+then
+    usage
+    exit 1
+fi
+
+BASE_COMMIT="$1"
+HEAD_COMMIT="$2"
+
+# git diff --check
+# uses .gitattributes to know what to check
+if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT";
+then
+    :
+else
+    >&2 echo "Whitespace errors!"
+    >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'."
+    >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
+    exit 1
+fi