From 588072fde350ae168ca10fd58e4a6c0a86756f02 Mon Sep 17 00:00:00 2001
From: David Li <li.davidm96@gmail.com>
Date: Tue, 30 Apr 2024 05:45:07 -0400
Subject: [PATCH] ci: disallow pings in PR body text

Fixes #1739.
---
 .github/workflows/dev_pr.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.github/workflows/dev_pr.yml b/.github/workflows/dev_pr.yml
index a001695cf5..805677cfb1 100644
--- 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