| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| |
| | |
This way, when editors leave over temporary files from editing
user-overlays, we don't prevent commits unless they are added to git.
|
|/
|
|
|
|
|
|
| |
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
| |
|
|
|
|
| |
[ci skip]
|
| |
|
|\ |
|
|\ \ |
|
| | | |
|
|/ /
| |
| |
| | |
OpenBSD mktemp fails with an error otherwise.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
```
$ dev/tools/check-owners-pr.sh 6809 --show-patterns --owner '@MSoegtropIMC'
remote: Counting objects: 93, done.
remote: Compressing objects: 100% (3/3), done.
remote: Total 93 (delta 47), reused 50 (delta 47), pack-reused 43
Unpacking objects: 100% (93/93), done.
From github.com:coq/coq
* branch refs/pull/6809/head -> FETCH_HEAD
* branch master -> FETCH_HEAD
/dev/build/windows: @MSoegtropIMC
```
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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 fulfils Gaetan's wish.
|
| |
| |
| |
| |
| |
| | |
In case the local branch is ahead of upstream, we only print
a warning because it could be that we are merging several
PRs in a row.
|
| |
| |
| |
| | |
As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
|
| |
| |
| |
| | |
This should solve Emilio's problem.
|
| |
| |
| |
| | |
In case the push URL has been overriden to make it fetch-only.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
```bash
$ dev/tools/check-owners.sh --show-patterns Makefile Makefile.build
/Makefile*: @letouzey
$ dev/tools/check-owners.sh --owner '@gares' stm/stm.ml interp/declare.ml
stm/stm.ml: @gares
$ dev/tools/check-owners.sh --show-patterns --owner '@gares' stm/*.ml interp/*.ml
/stm/: @gares
```
|
| |
| |
| |
| |
| | |
Can be used with git diff --name-only to identify owners for changes
in given commits.
|
|/ |
|
|
|
|
| |
This has come up a couple times.
|
|
|
|
|
| |
The script now performs many more checks and reports errors in
a more intelligible way.
|
|\ |
|
|\ \ |
|
| |/
|/|
| |
| |
| | |
That way you can just type [-j] instead of having to remember to add a
space yourself.
|
|\ \ |
|
| | |
| | |
| | |
| | | |
(and alist-alist)
|
| | | |
|
| | | |
|
| | | |
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| | | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Script modified from
https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status
I stuck the code in "install" rather than "before_install" so that the
lint target didn't need to be changed. I also haven't touched the
targets that add more packages; I'll leave that to someone who knows
more about the "&" and "*" syntax being used in the configuration.
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
We inline should-check-whitespace.sh in check-eof-newline.sh
simplifying the find invocation.
|
|\ \ \ \ |
|
| |_|/ /
|/| | | |
|