chore: Update branch name in GitHub Actions workflow

Parietal-INRIA · Jul 15, 2024 · d3b5cfa · d3b5cfa
1 parent 0426d3c
commit d3b5cfa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml
@@ -89,7 +89,7 @@ jobs:
 
     # Deploy the documentation to GitHub Pages.
     deploy_docs:
-        if: github.ref == 'refs/heads/main'
+        if: github.ref == 'refs/heads/master'
         needs: build_docs
         runs-on: ubuntu-latest
         steps: