diff --git a/.github/workflows/preview.yml b/.github/workflows/preview.yml index 15f35b84c..94c24fd2a 100644 --- a/.github/workflows/preview.yml +++ b/.github/workflows/preview.yml @@ -10,6 +10,10 @@ on: concurrency: group: docs +permissions: + contents: write + pull-requests: write + jobs: build-and-preview: if: github.event.action == 'opened' || github.event.action == 'synchronize' @@ -70,12 +74,7 @@ jobs: commit-message: Deploy preview for PR ${{ github.event.pull_request.number }} token: ${{ secrets.GITHUB_TOKEN }} - comment-preview-url: - needs: build-and-preview - if: needs.build-and-preview.result == 'success' - runs-on: ubuntu-latest - steps: - - name: Comment Preview URL + - name: Comment preview URL uses: thollander/actions-comment-pull-request@v2 with: message: | @@ -83,28 +82,3 @@ jobs: Preview the changes: https://turinglang.org/docs/pr-previews/${{ github.event.pull_request.number }} Please avoid using the search feature and navigation bar in PR previews! comment_tag: preview-url-comment - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - - delete-preview-directory: - if: github.event.action == 'closed' || github.event.pull_request.merged == true - runs-on: ubuntu-latest - steps: - - name: Checkout gh-pages branch - uses: actions/checkout@v4 - with: - ref: gh-pages - - - name: Remove PR Preview Directory - run: | - PR_NUMBER=${{ github.event.pull_request.number }} - PREVIEW_DIR="pr-previews/${PR_NUMBER}" - git config --global user.name "github-actions[bot]" - git config --global user.email "github-actions[bot]@users.noreply.github.com" - git pull origin gh-pages - rm -rf ${PREVIEW_DIR} - git add . - git commit -m "Remove preview for merged PR #${PR_NUMBER}" - git push - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/remove_preview.yml b/.github/workflows/remove_preview.yml new file mode 100644 index 000000000..40f67e619 --- /dev/null +++ b/.github/workflows/remove_preview.yml @@ -0,0 +1,31 @@ +name: Remove PR previews + +on: + pull_request_target: + types: + - closed + +permissions: + contents: write + +jobs: + delete-preview-directory: + if: github.event.action == 'closed' || github.event.pull_request.merged == true + runs-on: ubuntu-latest + steps: + - name: Checkout gh-pages branch + uses: actions/checkout@v4 + with: + ref: gh-pages + + - name: Remove PR Preview Directory + run: | + PR_NUMBER=${{ github.event.pull_request.number }} + PREVIEW_DIR="pr-previews/${PR_NUMBER}" + git config --global user.name "github-actions[bot]" + git config --global user.email "github-actions[bot]@users.noreply.github.com" + git pull origin gh-pages + rm -rf ${PREVIEW_DIR} + git add . + git commit -m "Remove preview for merged PR #${PR_NUMBER}" + git push