documentation/dev-guide.md

@@ -304,11 +304,63 @@ Depending on the situation, the merge should be handled by :
 
 You can :
 - check "Delete source branch"
-- "Squash commits" (especially if your developments contain many commits, it may be clearer for other users to read a summary of the changes related to the features instead of potentially a great number of commits containing bugs, etc.)
+- *optional*: "Squash commits" (especially if your developments contain many commits, it may be clearer for other users to read a summary of the changes related to the features instead of potentially a great number of commits containing bugs, etc.)
 - edit commit message for 2 reasons :
     1. Summarize the changes you propose to merge 
     2. Make sure your commit message complies with the commit message [push rule](#commit-rule)
 
+### Handling a merge conflict
+
+In case you have conflicting changes, Gitlab will raise a warning in the MR's overview tab: "Merge conflicts must be resolved.".
+
+If the merge conflicts are few and simple, Gitlab offers the possibility to interactively solve them in the Gitlab interface.
+
+In the case of complex merge conflicts, you must solve the conflicts locally. To do this:
+
+1. Checkout your feature branch (=the source branch)
+2. pull the target branch into your feature branch
+3. solve the conflicts where appropriate 
+
+For example, say you have a conflict when trying to merge branch `152-feature-foo-bar` into `develop`.
+
+1. Checkout branch `152-feature-foo-bar`:
+```shell
+git checkout 152-feature-foo-bar
+```
+2. Pull the target branch (`develop` from remote "public") into the source branch:
+```shell
+git pull public develop
+```
+3. The conflicts will be marked automatically by git. They look like this:
+```python
+import numpy as np
+<<<<<<< HEAD
+a = np.arange(0, 10+1, 1)
+=======
+a = np.linspace(0, 10, 11)
+>>>>>>> develop
+print(a)
+```
+Solve them, then add and commit the changes. To quote the [Github docs](https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/addressing-merge-conflicts/resolving-a-merge-conflict-using-the-command-line) :
+
+> Decide if you want to keep only your branch's changes, keep only the other 
+branch's changes, or make a brand new change, which may incorporate changes 
+from both branches. Delete the conflict markers <<<<<<<, =======, >>>>>>> and 
+make the changes you want in the final merge.
+
+After solving the conflict, the example code fragment could look like : 
+```python
+import numpy as np
+a = np.linspace(0, 10, 11)
+print(a)
+```
+All conflict markers have been removed (`<<<<<<< HEAD`, `=======` and 
+`>>>>>>> develop`), and only one statement declaring variable `a` was kept.
+
+Do `git add` on the files where conflicts were solved, then `git commit` with a 
+commit message describing the commit according to the push rules described 
+above.
+
 ## After a merge: `git fetch` or `git pull`
 
 After a merge (either on develop, main, or any other branch) occurs on Gitlab, run `git fetch` to update your local repository with the changes from remote, without merging them. Once you have fetched the changes from the remote repo, run `git merge` to merge the remote branch into your local branch (e.g. update your local develop branch with the latest changes from the Gitlab repo).