diff options
| author | Gaëtan Gilbert | 2019-06-06 15:56:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-06 17:59:08 +0200 |
| commit | cc2a10f1cfed35cb1ef193d23144bb10b45bcf21 (patch) | |
| tree | 3fdd4b431e5e143212577247a26dbb19546db043 /CONTRIBUTING.md | |
| parent | 8d2b88c80ec77090928a9da3d6b00e25a5ed6fb1 (diff) | |
Doc for per commit compile lint
Diffstat (limited to 'CONTRIBUTING.md')
| -rw-r--r-- | CONTRIBUTING.md | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index f0e17909c1..0d11d092ba 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -105,6 +105,12 @@ files end with newlines) is checked by the `lint` job on GitLab CI (using git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`. +Each commit in your pull request should compile (this makes bisecting +easier). The `lint` job checks compilation of the OCaml files, please +try to keep the rest of Coq in a functioning state as well. + +You may run the linter yourself with `dev/lint-repository.sh`. + Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. |