Merge branch 'minor-changes-gitlab-server' into 'develop'

minor changes as a result of gitlab migration

See merge request R3/howto-cards!275

external/contribute/vscode/vscode.md

@@ -75,14 +75,14 @@ If you need more details on how to do this, refer to the [corresponding howto-ca
 
     <img src="img/visual-code_img_13.png">
 
-## Step 6: Push to git-r3lab
+## Step 6: Push to the LCSB Gitlab server
 
 - When you push your procedure for the first time click on the cloud icon:
 
     <img src="img/visual-code_img_15.png">
 
 - Choose origin/"your gitlab user name"
-- Open git-r3lab: https://gitlab.lcsb.uni.lu/
+- Open Gitlab: https://gitlab.lcsb.uni.lu/
 
     <img src="img/visual-code_img_16.png">