diff options
| author | Théo Zimmermann | 2018-07-16 18:26:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-16 18:26:24 +0200 |
| commit | ec817cc2809a69bfff3c26353d1dc64ac59fe30b (patch) | |
| tree | e7065b51753d6e5f1aae8db9801b0c7dce0da94c | |
| parent | cca719d1feed89405db9109badf9adde15dadd99 (diff) | |
Mention the automatic use of the rebase label.
| -rw-r--r-- | CONTRIBUTING.md | 3 |
1 files changed, 3 insertions, 0 deletions
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. |