Auto-create .git/hooks/pre-commit on ./configure

The hook created checks to see if dev/tools/pre-commit exists, and, if
so, runs it.  This way, we don't have to do any fancy logic to update
the git pre-commit hook.  The configure script never overwrites an
existing precommit hook, so users can disable it by creating an empty
pre-commit hook.

The check for existence is so that if users check out an old version of
Coq, attempting to commit won't give an error about non-existent files.

1 files changed, 16 insertions, 0 deletions

diff --git a/configure.ml b/configure.ml
index 06a7dd822..2b08a0ff0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -451,6 +451,22 @@ let vcs =
   else if dir_exists "{arch}" then "gnuarch"
   else "none"
 
+(** * Git Precommit Hook *)
+let _ =
+  let f = ".git/hooks/pre-commit" in
+  if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
+    printf "Creating pre-commit hook in %s\n" f;
+    let o = open_out f in
+    let pr s = fprintf o s in
+    pr "#!/bin/sh\n";
+    pr "\n";
+    pr "if [ -x dev/tools/pre-commit ]; then\n";
+    pr "    exec dev/tools/pre-commit\n";
+    pr "fi\n";
+    close_out o;
+    Unix.chmod f 0o775
+  end
+
 (** * Browser command *)
 
 let browser =