From 3a4f626edd44bb9f6625735e0647b8ff3447b5f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lars=20G=C3=B6ttgens?= Date: Mon, 20 Nov 2023 10:10:27 +0100 Subject: [PATCH] Update doc preview cleanup CI job --- ...nupDocPreview.yml => DocPreviewCleanup.yml} | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) rename .github/workflows/{CleanupDocPreview.yml => DocPreviewCleanup.yml} (57%) diff --git a/.github/workflows/CleanupDocPreview.yml b/.github/workflows/DocPreviewCleanup.yml similarity index 57% rename from .github/workflows/CleanupDocPreview.yml rename to .github/workflows/DocPreviewCleanup.yml index e7b76bda..72fc16a6 100644 --- a/.github/workflows/CleanupDocPreview.yml +++ b/.github/workflows/DocPreviewCleanup.yml @@ -1,29 +1,31 @@ -name: Cleanup Doc Preview +name: Doc Preview Cleanup on: pull_request: types: [closed] jobs: - cleanup-doc-preview: + doc-preview-cleanup: runs-on: ubuntu-latest + permissions: + contents: write steps: - name: Checkout gh-pages branch - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: ref: gh-pages - - name: Delete preview + - name: Delete preview and history + push changes run: | if [ -d "previews/PR$PRNUM" ]; then git config user.name "Documenter.jl" git config user.email "documenter@juliadocs.github.io" git rm -rf "previews/PR$PRNUM" - git commit -m "delete preview for $PRNUM" - git push origin gh-pages:gh-pages + git commit -m "delete preview" + git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree}) + git push --force origin gh-pages-new:gh-pages fi env: PRNUM: ${{ github.event.number }} -# adapted from here: +# copied from here: # https://juliadocs.github.io/Documenter.jl/stable/man/hosting/#gh-pages-Branch -# without history cleanup