diff options
| author | Jason Gross | 2018-01-16 08:31:08 -0500 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-08 17:15:02 +0100 |
| commit | d31777adb88eb5ba54f68ac7a4cb7a2a29c1fc20 (patch) | |
| tree | dcf16936a2c05dc89a65c0f4632152b4d4523035 /dev/tools | |
| parent | 95ee1fe61d3623b2d07f1806520de591536976f2 (diff) | |
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.
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/pre-commit | 3 |
1 files changed, 2 insertions, 1 deletions
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 |