aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/pre-commit
AgeCommit message (Collapse)Author
2018-03-31pre-commit: verify user overlay extensions (must be .sh).Gaëtan Gilbert
This has come up a couple times.
2018-02-08pre-commit: nicer messagesGaëtan Gilbert
2018-02-08pre-commit: fail gracefully if fixing whitespace removes all changesGaëtan Gilbert
2018-02-08pre-commit: add files after fixing ending newlines.Gaëtan Gilbert
2018-02-08Have the pre-commit hook also fix end-of-file nlJason Gross
2018-02-08Auto-create .git/hooks/pre-commit on ./configureJason Gross
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.
2018-02-08pre-commit hook: fix whitespace error detectionGaëtan Gilbert
--quiet implies --exit-code
2018-02-08A pre-commit hook to magically fix whitespace issues.Gaëtan Gilbert