Commit ce65e700 authored by Guillaume Pasero's avatar Guillaume Pasero

DOC: clarification about pushing directly on develop

parent 4b99a1e3
......@@ -58,6 +58,11 @@ then send a merge request.
Note that we also accept PRs on our [GitHub mirror](
which we will manually merge.
Caveat: if the Dashboard build on develop branch is broken, it is possible for
core developers to push their fixes directly on develop (to gain time) but this
is strictly limited to compilation error fixes. It is assumed that core
developers are aware of the multi-platform environment on the Dashboard.
### Commit message
On your feature branch, write a good [commit message](
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment