Merge branch 'develop' into 'master'

Regular merge of develop

See merge request R3.training/git.slides!32

.gitlab-ci.yml

@@ -19,7 +19,7 @@ pages:
     - mv public/* stable/.
 
     # build the develop version into latest
-    - git checkout develop
+    - git checkout -f develop
     - git fetch origin develop
     - git reset --hard origin/develop
     - grunt dist