ci: allow manual deployment to GitHub Pages via workflow inputs

Author: d-biehl

.github/workflows/deploy-docs.yml

@@ -13,6 +13,11 @@ on:
 
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
+    inputs:
+      deploy:
+        description: "Deploy to GitHub Pages"
+        type: boolean
+        default: false
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
@@ -55,7 +60,7 @@ jobs:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
     needs: build
-    if: success() && startsWith( github.ref, 'refs/tags/v')
+    if: success() && (startsWith( github.ref, 'refs/tags/v') || inputs.deploy == true)
     runs-on: ubuntu-latest
     name: Deploy
     steps: