From ed9d2d3d9eb9ea56f622eee050f0ab18ac7294aa Mon Sep 17 00:00:00 2001
From: Garry O'Donnell <garry.o'donnell@diamond.ac.uk>
Date: Wed, 19 Jul 2023 18:50:28 +0100
Subject: [PATCH] Publish to GitHub pages on push to main

---
 .github/workflows/docs.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 74e2b277..c98b1886 100644
--- 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