From ec817cc2809a69bfff3c26353d1dc64ac59fe30b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 16 Jul 2018 18:26:24 +0200
Subject: Mention the automatic use of the rebase label.

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

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index d9b36241ae..cd4a246bb4 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -60,6 +60,9 @@ Here are a few tags Coq developers may add to your PR and what they mean. In gen
   the latest base branch (usually `master`). See the
   [GitHub documentation](https://help.github.com/articles/about-git-rebase/)
   for a brief introduction to using `git rebase`.
+  This label will be automatically added if you open or synchronize your PR and
+  it is not up-to-date with the base branch. So please, do not forget to rebase
+  your branch every time you update it.
 - [needs: fixing][fixing-label] indicates the PR needs a fix, as discussed in the comments.
 - [needs: benchmarking][benchmarking-label] and [needs: testing][testing-label]
   indicate the PR needs testing beyond what the test suite can handle.
-- 
cgit v1.2.3