| Age | Commit message (Collapse) | Author |
|---|
|
OpenBSD mktemp fails with an error otherwise.
|
|
Having `--whitespace=` on all `git apply` in this script should make it
insensitive to user setup in `~/.gitconfig`, at least
`[apply] whitespace = fix`.
Note that even this way, this script remains hugely fragile and non mature,
and would better *not* be set by default for everybody.
|
|
This has come up a couple times.
|
|
|
|
|
|
|
|
|
|
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.
|
|
--quiet implies --exit-code
|
|
|
