Build old docs as part of deployment to GitHub Pages

Author: alexdewar

.github/workflows/deploy-docs.yml

@@ -23,7 +23,16 @@ jobs:
     steps:
       - name: Checkout repository
         uses: actions/checkout@v6
+        with:
+          fetch-tags: true
+      - name: Set user name and email for git
+        run: |
+          # Needed so we can apply patches
+          git config --global user.name "GitHub Actions"
+          git config --global user.email "github-actions[bot]@users.noreply.github.com"
       - uses: ./.github/actions/generate-docs
+        with:
+          build: all_with_old
       - name: Setup pages
         uses: actions/configure-pages@v5
       - name: Upload artifact