Added git hooks for lexical syntax checking.

tools/git-hooks/README

@@ -0,0 +1,15 @@
+This directory holds two shell scripts that can be used in conjunction with git
+to reject commits containing ill-formed .ml / .mli files. Are considered
+ill-formed files that contain:
+
+* Trailing whitespace.
+* Lines spanning more than 80 columns.
+* Tab characters.
+
+The "pre-commit" and "update" scripts respectively handle local commits ("git
+commit") and remote calls to "git push". To enable a script, just copy it to
+$GIT_DIR/hooks/.
+
+For more information, refer to the githooks manual page.
+
+-- Adrien Guatto

tools/git-hooks/pre-commit

@@ -0,0 +1,36 @@
+#!/bin/sh
+
+bad=0
+
+check_file() {
+  name=$1
+  tmp=$2
+
+  if [ `wc -L $tmp | awk '{ print $1 }'` -gt 80 ]; then
+    echo "File \"$name\" has lines with more than 80 columns."
+    bad=1
+  fi
+
+  grep -P '\t' $tmp > /dev/null
+  if [ $? -eq 0 ]; then
+    echo "File \"$name\" has tabulations in it."
+    bad=1
+  fi
+
+  grep -P '( |\t)+$' $tmp > /dev/null
+  if [ $? -eq 0 ]; then
+    echo "File \"$name\" has trailing whitespace."
+    bad=1
+  fi
+}
+
+for f in $(git diff-index --cached --name-only HEAD --diff-filter=ACMR | egrep "\.ml(i?)$")
+do
+  tf=$(git checkout-index --temp $f | cut -f 1)
+  trap "rm -f -- $tf" EXIT
+  check_file $f $tf
+  rm -f -- $tf
+  trap - EXIT
+done
+
+exit $bad

tools/git-hooks/update

@@ -0,0 +1,72 @@
+#!/bin/sh
+# Check for lexical syntax of commits in the current push that
+
+refname="$1"
+oldrev="$2"
+newrev="$3"
+
+if [ -z "$GIT_DIR" ]; then
+  echo "Don't run this script from the command line." >&2
+  echo " (if you want, you could supply GIT_DIR then run" >&2
+  echo "  $0 <ref> <oldrev> <newrev>)" >&2
+  exit 1
+fi
+
+if [ -z "$refname" -o -z "$oldrev" -o -z "$newrev" ]; then
+  echo "Usage: $0 <ref> <oldrev> <newrev>" >&2
+  exit 1
+fi
+
+# --- Check types
+# if $newrev is 0000...0000, it's a commit to delete a ref.
+zero="0000000000000000000000000000000000000000"
+if [ "$newrev" = "$zero" ]; then
+  newrev_type=delete
+else
+  newrev_type=$(git cat-file -t $newrev)
+fi
+
+# Good commit by default
+bad=0
+
+IFS='
+'
+
+# If the new object is a commit...
+if [ "$newrev_type" = "commit" ]; then
+  # Loop over the new revisions
+  for c in $(git rev-list $old_rev..$newrev); do
+    # And each new file
+    for s in $(git ls-tree $c | egrep '\.ml(i?)$'; do
+      f=$(echo $s | awk '{ print $3 }')
+      name=$(echo $s | awk '{ print $4 }')
+      tmp=$(tempfile) || exit 1
+      trap "rm -f -- '$tmp'" EXIT
+      git cat-file blob $f > $tmp
+      # $tmp now holds the content of new file $name
+
+      if [ `wc -L $tmp | awk '{ print $1 }'` -gt 80 ]; then
+        echo "Commit $c/File \"$name\" has lines with more than 80 columns."
+        bad=1
+      fi
+
+      grep -P '\t' $tmp > /dev/null
+      if [ $? -eq 0 ]; then
+        echo "Commit $c/File \"$name\" has tabulations in it."
+        bad=1
+      fi
+
+      grep -P '( |\t)+$' $tmp > /dev/null
+      if [ $? -eq 0 ]; then
+        echo "Commit $c/File \"$name\" has trailing whitespace."
+        bad=1
+      fi
+
+      # Delete temporary file and remove the associated trap
+      rm -f -- '$tmp'
+      trap - EXIT
+    done
+  done
+fi
+
+exit $bad