From 0ad8eab61302c55b93a346d14e60969e5c9c45c8 Mon Sep 17 00:00:00 2001
From: Martin Costello <martin@martincostello.com>
Date: Sat, 28 Oct 2023 19:27:33 +0100
Subject: [PATCH] Prevent concurrent page builds

If multiple PRs are merged in succession, don't try and try and update GitHub Pages from multiple workflow runs at the same time.
---
 .github/workflows/gh-pages.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml
index 4ff94c036f0..f6be7ee5caa 100644
--- a/.github/workflows/gh-pages.yml
+++ b/.github/workflows/gh-pages.yml
@@ -14,6 +14,10 @@ jobs:
   publish-docs:
     runs-on: ubuntu-latest
 
+    concurrency:
+      group: ${{ github.workflow }}
+      cancel-in-progress: false
+
     permissions:
       contents: write
       pages: write