"Delete PR staging and head branches" workflow fails for PR merges by 'advisory-database' bot #5167
Description
The "Delete PR staging and head branches" (.github/workflows/delete_staging_and_head_branches.yaml
) workflow currently fails when a PR was merged by the 'advisory-database' bot, because that bot is already deleting the source branch itself.
This might be a bit irritating when viewing the "Checks" tab of a pull request, or when you see the ❌ indicator for the commit of the pull request.
See for example https://github.com/github/advisory-database/actions/runs/12750406199 for #4588.
Maybe the solution could be that the 'advisory-database' bot is changed to not delete the branch itself?
Removing the "Delete PR staging and head branches" workflow is probably not an option because it is needed for pull requests closed by the author (and not merged), and adding || true
or similar in the workflow might hide actual errors when deleting branches.