From cc2a10f1cfed35cb1ef193d23144bb10b45bcf21 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Jun 2019 15:56:35 +0200
Subject: Doc for per commit compile lint

---
 CONTRIBUTING.md | 6 ++++++
 1 file changed, 6 insertions(+)

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.
-- 
cgit v1.2.3