Build pdf docs too

Author: kwankyu

.github/workflows/doc-build-pdf.yml

@@ -148,3 +148,36 @@ jobs:
         with:
           name: doc-pdf
           path: doc-pdf.zip
+
+      #
+      # On release events
+      #
+
+      - name: Build live doc
+        if: github.event_name != 'pull_request'
+        run: |
+          # Avoid running out of disk space
+          rm -rf upstream
+          export SAGE_USE_CDNS=yes
+          export SAGE_LIVE_DOC=yes
+          export SAGE_JUPYTER_SERVER=binder:sagemath/sage-binder-env/dev
+          make doc-clean doc-uninstall
+          ./config.status && make sagemath_doc_html-no-deps
+        shell: sh .github/workflows/docker-exec-script.sh BUILD /sage {0}
+
+      - name: Copy live doc
+        if: github.event_name != 'pull_request'
+        run: |
+          mkdir -p ./livedoc
+          # We copy everything to a local folder
+          docker cp --follow-link BUILD:/sage/local/share/doc/sage/html livedoc
+          docker cp --follow-link BUILD:/sage/local/share/doc/sage/pdf livedoc
+          docker cp --follow-link BUILD:/sage/local/share/doc/sage/index.html livedoc
+          zip -r livedoc.zip livedoc
+
+      - name: Upload live doc
+        if: github.event_name != 'pull_request'
+        uses: actions/upload-artifact@v4
+        with:
+          name: livedoc
+          path: livedoc.zip

.github/workflows/doc-build.yml

@@ -204,32 +204,3 @@ jobs:
         with:
           name: doc-${{ github.ref_name }}
           path: doc.zip
-
-      - name: Build live doc
-        if: github.event_name != 'pull_request'
-        shell: bash -l {0}
-        run: |
-          # Remove previous doc build
-          rm -rf builddir/src/doc
-          meson compile -C builddir doc-html -j1
-        env:
-          SAGE_USE_CDNS: yes
-          SAGE_LIVE_DOC: yes
-          SAGE_JUPYTER_SERVER: binder:sagemath/sage-binder-env/dev
-
-      - name: Copy live doc
-        if: github.event_name != 'pull_request'
-        run: |
-          mkdir -p ./livedoc
-          # We copy everything to a local folder
-          cp -r builddir/src/doc/html livedoc/
-          cp builddir/src/doc/index.html livedoc/
-          zip -r livedoc.zip livedoc
-
-      - name: Upload live doc
-        if: github.event_name != 'pull_request'
-        uses: actions/upload-artifact@v4
-        with:
-          name: livedoc
-          path: livedoc.zip
-

.github/workflows/doc-publish.yml

@@ -2,7 +2,7 @@ name: Publish documentation
 
 on:
   workflow_run:
-    workflows: ["Build documentation"]
+    workflows: ["Build documentation", "Build documentation (PDF)"]
     types:
       - completed
 
@@ -12,8 +12,8 @@ permissions:
   pull-requests: write
 
 
-# This workflow runs after doc-build workflow, taking the artifact
-# (doc/livedoc) and deploying it to a netlify site.
+# This workflow runs after doc-build and doc-build-pdf workflows, taking the
+# artifact (doc/livedoc) and deploying it to a netlify site.
 #
 # event (triggered doc-build)     URL (of the doc deployed to NETLIFY_SITE)
 # ---------------------------     ---------------------------------