From b33794516f4dd10edcb06be49c0202a9e056c26e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 Oct 2018 14:26:32 +0200
Subject: [ci] [doc] Notes about branch names.

I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
---
 dev/ci/user-overlays/README.md | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'dev/ci/user-overlays')

diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 68afe7ee4a..7fb73e447d 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -33,3 +33,11 @@ fi
 ```
 
 (`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
+
+### Branching conventions
+
+We suggest you use the convention of identical branch names for the
+Coq branch and the CI project branch used in the overlay. For example,
+if your Coq PR is coming from the branch `more_efficient_tc`, and that
+breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch
+named `more_efficient_tc`.
-- 
cgit v1.2.3