Publish to GitHub pages on push to main

DiamondLightSource · Jul 20, 2023 · ed9d2d3 · ed9d2d3
1 parent 607838c
commit ed9d2d3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -47,7 +47,7 @@ jobs:
           path: target/doc
 
   publish:
-    if: github.event_name == 'push' && github.head_ref == 'main'
+    if: github.event_name == 'push' && github.ref == 'refs/heads/main'
     runs-on: ubuntu-latest
     permissions:
       pages: write