Separate preview + remove-preview workflows

.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,41 +74,11 @@ 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: |
             <!-- preview-url-comment -->
             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 }}

.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