ci: Update aliases when deploying with mike (#38)

This is needed because we expect aliases we are deploying to already
exist, and mike by default will only create new aliases, but not "move"
them.

For example, if the current stable is v0.10.0 (`mike` version will be
`v0.10` and `latest` and `v0` will point to it) and we just released
v0.11.0, then the `latest` and `v0` aliases will need to be changed to
point to `v0.11`.

For more details see:
https://github.com/jimporter/mike#building-your-docs

Author: llucax

.github/workflows/ci.yaml

@@ -174,7 +174,7 @@ jobs:
           VERSION: ${{ steps.mike-metadata.outputs.version }}
           ALIASES: ${{ steps.mike-metadata.outputs.aliases }}
         run: |
-          mike deploy --push "$VERSION" $ALIASES
+          mike deploy --push --update-aliases "$VERSION" $ALIASES
 
   create-github-release:
     needs: ["publish-docs"]