`pr-body` workflow doesn't pick up on labels added by `labels-from-comments` workflow

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The pr-body workflow checks that a changelog- label is present; however, upon adding a changelog label through a comment, the workflow check isn't retriggered, meaning that you have to retrigger through other means, e.g. by pushing an empty commit or editing the PR description.

Context

This happened frequently to me (and also definitely others) but I always forgot to report it.

Steps to Reproduce

1. Create a (non-draft) PR to this repository with the title starting with feat or fix and a description starting with This PR .
2. Wait for the pr-body workflow to fail (this is expected)
3. Add a changelog label by sending a comment with the name of such a label, e.g. changelog-library.

Expected behavior: The pr-body workflow gets rerun and succeeds.

Actual behavior: The pr-body workflow doesn't get run again, leaving it in a failed state, making it necessary to resort to other means (e.g. editing the PR description) to retrigger it.

Versions

N/A

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Inspect the GitHub Actions definitions for the pr-body and labels-from-comments workflows, then reproduce the sequence of a failed pr-body check followed by adding a changelog- label in a comment. Done means adding the label causes pr-body to run again and succeed without an unrelated PR change.