Merge pull request #1457 from flintlib/alexjbest-patch-1

fix doc build
flintlib · Oct 9, 2023 · 40d1a53 · 40d1a53
2 parents ed28411 + f0f648c
commit 40d1a53
Showing 1 changed file with 1 addition and 7 deletions.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -45,17 +45,11 @@ jobs:
           cd doc
           make html SPHINXOPTS="-W -j auto"
 
-      - name: "Build documentation"
-        if: success() && steps.check_doc_changes.outputs.diff == 'true'
-        run: |
-          cd doc
-          make html SPHINXOPTS="-W -j auto"
-
       - name: "Build pdf documentation"
         if: success() && steps.check_doc_changes.outputs.diff == 'true'
         run: |
           cd doc
-          make latex SPHINXOPTS="-W -j auto"
+          make latexpdf SPHINXOPTS="-W -j auto"
 
       - name: "Create a tarball of the documentation"
         if: success() && steps.check_doc_changes.outputs.diff == 'true'