diff options
| -rw-r--r-- | configure.ml | 16 | ||||
| -rwxr-xr-x | dev/tools/pre-commit | 3 |
2 files changed, 18 insertions, 1 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 = diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index ce8bc67df..59cc84856 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 |