From 1cb69ba7e97c22a38d4036bc30bb55dacd62cebe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Albin=20Ahlb=C3=A4ck?= Date: Mon, 27 Oct 2025 23:32:51 +0100 Subject: [PATCH] Only build PDF when deploying Saves a couple minutes on the CI --- .github/workflows/docs.yml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 9254c57f69..2c60154383 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -32,8 +32,6 @@ jobs: run: | sudo apt-get update sudo apt-get install -y python3-sphinx - # See https://www.sphinx-doc.org/en/master/usage/builders/index.html#sphinx.builders.latex.LaTeXBuilder - sudo apt-get install -y texlive-latex-recommended texlive-fonts-recommended texlive-fonts-extra tex-gyre texlive-latex-extra latexmk sphinx-build --version - name: "Build documentation" @@ -41,7 +39,14 @@ jobs: cd doc make html SPHINXOPTS="-W -j auto" + - name: "Setup LaTeX" + if: github.repository == 'flintlib/flint' && github.event_name == 'push' && github.ref == 'refs/heads/main' + run: | + # See https://www.sphinx-doc.org/en/master/usage/builders/index.html#sphinx.builders.latex.LaTeXBuilder + sudo apt-get install -y texlive-latex-recommended texlive-fonts-recommended texlive-fonts-extra tex-gyre texlive-latex-extra latexmk + - name: "Build PDF documentation" + if: github.repository == 'flintlib/flint' && github.event_name == 'push' && github.ref == 'refs/heads/main' run: | cd doc make latexpdf SPHINXOPTS="-W -j auto"