PR associated with default branch

Stream: mathlib4

[Filippo A. E. Nuccio]

When I clone a fresh version of mathlib, I get a message from VSCode telling me that

There's a pull request associated with the default branch 'master'. Do you want to ignore this Pull Request?

I suspect it is #7215. Where does the message come from?

[Alex J. Best]

I think it comes from the Github Pull requests and issues vscode extension, I would also like to get rid of it but don't know how

[Alex J. Best]

Ok I made #7807