fix: linter should have access to all messages, really

[Kha]

Continuation of #8101

[leanprover-community-bot]

• ✅ Mathlib branch lean-pr-testing-8117 has successfully built against this PR. (2025-04-26 14:46:22) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 18f8a18bfcadfce98d4285deeaba97cdc53cfef1 --onto 416e07a68e5d9b884de8af4836497a7cc2414c8f. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-26 15:29:12)

[github-actions]

The backport to releases/v4.19.0 failed:

The process '/usr/bin/git' failed with exit code 1

To backport manually, run these commands in your terminal:

# Fetch latest updates from GitHub
git fetch
# Create a new working tree
git worktree add .worktrees/backport-releases/v4.19.0 releases/v4.19.0
# Navigate to the new working tree
cd .worktrees/backport-releases/v4.19.0
# Create a new branch
git switch --create backport-8117-to-releases/v4.19.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 82723489c96e8e832d8b1b7f117f1767a0bcd071
# Push it to GitHub
git push --set-upstream origin backport-8117-to-releases/v4.19.0
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-releases/v4.19.0

Then, create a pull request where the base branch is releases/v4.19.0 and the compare/head branch is backport-8117-to-releases/v4.19.0.