ci: disallow pings in PR body text

Fixes apache#1739.
lidavidm · Apr 30, 2024 · 8c62e0e · 8c62e0e
1 parent 8686e6c
commit 8c62e0e
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/.github/workflows/dev_pr.yml b/.github/workflows/dev_pr.yml
@@ -57,3 +57,11 @@ jobs:
           PR_TITLE: ${{ github.event.pull_request.title }}
         run: |
           python .github/workflows/dev_pr/title_check.py $(pwd)/pr_checkout "$PR_TITLE"
+
+      # Pings make it into the commit message where they annoy the user every
+      # time the commit gets pushed somewhere
+      - Name: Check PR body for pings
+        env:
+          PR_BODY: ${{ github.event.pull_request.body }}
+        run: |
+          [[ "${PR_BODY}" =~ @[a-zA-Z0-9]+ ]] && exit 1 || true