GitHub: wrong blocked-by label from bot

Stream: mathlib4

[Thomas Murrills]

This is quite minor, but just wanted to report that I noticed on #6928 that the leanprover-community-mathlib4-bot added the blocked-by-other-PR label in response to being marked as dependent on a core PR; am I right in thinking that PRs like this should instead get labeled blocked-by-core-PR by the bot?

[Scott Morrison]

Our CI uses https://github.com/z0al/dependent-issues, which unfortunately doesn't allow for customisation of labels depending on the location of the upstream PR.

I think that if you change the labels yourself the bot doesn't fight you.