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