💚(docs) add docs versioning in CI

With the help of `mike`, change the `deploy-docs` job to deploy docs with
versioning.
Job is executed for tags and for the master branch.
Example:
- For tags, docs will be tagged with the version 1.1 (for git tag v1.1.2)
and alias "latest"
- For master branch, docs will be tagged with version `dev` without any alias.

.circleci/config.yml

@@ -495,8 +495,17 @@ jobs:
           command: |
             git config --global user.email "[email protected]"
             git config --global user.name "FUN MOOC Bot"
-            ~/.local/bin/mkdocs gh-deploy
-
+            # Deploy docs with either:
+            # - DOCS_VERSION: 1.1 (for git tag v1.1.2)
+            # - DOCS_ALIAS: latest
+            # or
+            # - DOCS_VERSION: dev (for master branch)
+            # - No DOCS_ALIAS
+            DOCS_VERSION=$([[ -z "$CIRCLE_TAG" ]] && echo $CIRCLE_BRANCH || echo ${CIRCLE_TAG} | sed 's/^v\([0-9]\.[0-9]*\)\..*/\1/')
+            DOCS_ALIAS=$([[ -z "$CIRCLE_TAG" ]] && echo "" || echo "latest")
+            echo "DOCS_VERSION: ${DOCS_VERSION}"
+            echo "DOCS_ALIAS: ${DOCS_ALIAS}"
+            ~/.local/bin/mike deploy --push --update-aliases ${DOCS_VERSION} ${DOCS_ALIAS}
   # Make a new github release
   release:
     docker:
@@ -680,7 +689,7 @@ workflows:
             branches:
               only: master
             tags:
-              only: /.*/
+              only: /^v.*/
 
       # Release
       - release: