Updated building of docs in CI

Fixes #54
JCGoran · Apr 11, 2023 · 292f41d · 292f41d
1 parent 3f5219e
commit 292f41d
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/.github/workflows/build-docs.yml b/.github/workflows/build-docs.yml
@@ -33,8 +33,14 @@ jobs:
       run: |
         bash generate_docs.sh
 
-    # If we've pushed to master, push the book's HTML to github-pages
-    - if: ${{ github.ref == 'refs/heads/master' }}
+    # If we've pushed to master with a tag, push the book's HTML to github-pages
+    - name: Check Tag
+      id: check-tag
+      run: |
+        if [[ ${{ github.event.ref }} =~ ^refs/tags/[0-9]+\.[0-9]+\.[0-9]+$ ]]; then
+            echo "match=true" >> $GITHUB_OUTPUT
+        fi
+      if: steps.check-tag.outputs.match == 'true'
       name: GitHub Pages action
       uses: peaceiris/actions-gh-pages@v3
       with: