From 3d54860abf30ee8a8022c4889c33d6027cf02713 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mos=C3=A8=20Giordano?= <mose@gnu.org>
Date: Sun, 26 Jan 2025 17:03:28 +0000
Subject: [PATCH] [CI] Add workflow to clean up docs previews

---
 .github/workflows/Documenter.yaml    | 18 +++++++++++------
 .github/workflows/PreviewCleanup.yml | 30 ++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 6 deletions(-)
 create mode 100644 .github/workflows/PreviewCleanup.yml

diff --git a/.github/workflows/Documenter.yaml b/.github/workflows/Documenter.yaml
index 8155961e1f..b7e51cc450 100644
--- a/.github/workflows/Documenter.yaml
+++ b/.github/workflows/Documenter.yaml
@@ -3,7 +3,7 @@ name: Documentation
 on:
   pull_request:
     paths:
-      - '.github/workflows/Documenter.yml'
+      - '.github/workflows/Documenter.yaml'
       - 'docs/**'
       - 'lib/**'
       - 'src/**'
@@ -12,21 +12,27 @@ on:
       - main
     tags: '*'
     paths:
-      - '.github/workflows/Documenter.yml'
+      - '.github/workflows/Documenter.yaml'
       - 'docs/**'
       - 'lib/**'
       - 'src/**'
 
 concurrency:
-  # Skip intermediate builds: always.
-  # Cancel intermediate builds: only if it is a pull request build.
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }}
+  # Same group concurrency as the `PreviewCleanup.yml` workflow, because they both
+  # git-push to the same branch, so we want to avoid clashes.  NOTE: this is
+  # different from the concurrency group below, which is to cancel successive
+  # jobs from within the PR.
+  group: docs-pushing
 
 jobs:
   docs:
     name: Documentation
     runs-on: ubuntu-latest
+    concurrency:
+      # Skip intermediate builds: always.
+      # Cancel intermediate builds: only if it is a pull request build.
+      group: ${{ github.workflow }}-${{ github.ref }}
+      cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }}
     steps:
       - uses: actions/checkout@v4
       - uses: julia-actions/setup-julia@v2
diff --git a/.github/workflows/PreviewCleanup.yml b/.github/workflows/PreviewCleanup.yml
new file mode 100644
index 0000000000..a9fb18f576
--- /dev/null
+++ b/.github/workflows/PreviewCleanup.yml
@@ -0,0 +1,30 @@
+name: Doc Preview Cleanup
+
+on:
+  pull_request:
+    types: [closed]
+
+concurrency:
+  # Same group concurrency as the `docs.yml` workflow, because they both
+  # git-push to the same branch, so we want to avoid clashes.
+  group: docs-pushing
+
+jobs:
+  doc-preview-cleanup:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout gh-pages branch
+        uses: actions/checkout@v4
+        with:
+          ref: gh-pages
+      - name: Delete preview and history + push changes
+        run: |
+          preview_directory=preview/PR${{ github.event.number }}
+            if [[ -d "${preview_directory}" ]]; then
+              git config user.name "${{github.actor}}"
+              git config user.email "${{github.actor_id}}+${{github.actor}}@users.noreply.github.com"
+              git rm -rf "${preview_directory}"
+              git commit -m 'Cleanup docs for PR #${{ github.event.number }}'
+              git branch gh-pages-new $(echo "Delete history" | git commit-tree HEAD^{tree})
+              git push --force origin gh-pages-new:gh-pages
+            fi