Delete dev ddocumentation before deployment to force update

Signed-off-by: Federico Busetti <[email protected]>

.github/workflows/github-pages-dev.yml

@@ -14,3 +14,4 @@ jobs:
     uses: ./.github/workflows/reusable-github-pages.yml
     with:
       site-version: "dev"
+      delete-before-deploy: true

.github/workflows/reusable-github-pages.yml

@@ -16,6 +16,10 @@ on:
         required: false
         type: boolean
         default: false
+      delete-before-deploy:
+        required: false
+        type: boolean
+        default: false
 
 # Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
 # However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
@@ -60,6 +64,12 @@ jobs:
         run: |
           git fetch origin gh-pages --depth=1
 
+      - name: Delete existing version
+        if: ${{ inputs.delete-before-deploy }}
+        continue-on-error: true
+        run: |
+          mike delete ${{ inputs.site-version }} --branch ${{ inputs.branch }}
+
       - name: Build and deploy static pages
         run: |
           mike deploy ${{ inputs.site-version }} ${{ inputs.version-alias }} --update-aliases --push --branch ${{ inputs.branch }}