Note that this workflow currently imagines writing a comment.
It does not actually try to do so, and thus there is no need to ask
for permission to use `pull-requests: write`.
If at some point, someone decides to fix that feature, they
will need to add that permission.
OTOH, using a GitHub Step Summary instead does not require any permissions.