From 9b9e717c41beeba765cdcef7f833f22989c2f614 Mon Sep 17 00:00:00 2001
From: Romain Vimont <rom@rom1v.com>
Date: Tue, 7 Apr 2020 10:38:13 +0200
Subject: [PATCH] Explain master and dev branches in BUILD

People may not guess that `master` is not the development branch.
---
 BUILD.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/BUILD.md b/BUILD.md
index e35d07d0..9f49216e 100644
--- a/BUILD.md
+++ b/BUILD.md
@@ -8,6 +8,22 @@ case, use the [prebuilt server] (so you will not need Java or the Android SDK).
 
 [prebuilt server]: #prebuilt-server
 
+## Branches
+
+### `master`
+
+The `master` branch concerns the latest release, and is the home page of the
+project on Github.
+
+
+### `dev`
+
+`dev` is the current development branch. Every commit present in `dev` will be
+in the next release.
+
+If you want to contribute code, please base your commits on the latest `dev`
+branch.
+
 
 ## Requirements