documentation/dev-guide.md

@@ -7,6 +7,7 @@ title: Developer guide
 
 
 
+
 # IMPORTANT 
 
 If you have a local clone of the repository that **predates Feb. 19th, 2025, you must absolutely make a new clone**. 
@@ -269,12 +270,17 @@ Approval will be granted if your changes:
 Once an MR is approved, you can prepare to merge it in the target branch (typically, feature branches merge into develop).
 
 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.)
+- 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.)
 - 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)
 
+## 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. Run `git pull` to merge the remote changes into your local repository.
+
+Read more here: [Getting changes from a remote repository](https://docs.github.com/en/get-started/using-git/getting-changes-from-a-remote-repository)
 
 # Good practices