From d31777adb88eb5ba54f68ac7a4cb7a2a29c1fc20 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 16 Jan 2018 08:31:08 -0500
Subject: 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.
---
 dev/tools/pre-commit | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'dev/tools/pre-commit')

diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index ce8bc67df2..59cc84856d 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -1,6 +1,7 @@
 #!/bin/sh
 
-# Copy to .git/hooks/ to use.
+# configure automatically sets up a wrapper at .git/hooks/pre-commit
+# which calls this script (if it exists).
 
 set -e
 
-- 
cgit v1.2.3