github question

Stream: mathlib4

[Kevin Buzzard]

I'm going through my github notifications and I notice that in the majority of them, two commits which I can't find (always by the same people) apparently "reference the PR" (despite the PRs being on wildly different topics). What's going on here?

e.g.

Screenshot-from-2024-05-19-14-38-27.png
Screenshot-from-2024-05-19-14-37-56.png

[Yaël Dillies]

They added the commit actually referencing the PR to their PR, probably by merging?

[Rida Hamadani]

You do it too:
pushedcommit.png

[Mario Carneiro]

This sounds kind of like how I get regular pings like https://github.com/leanprover-community/mathlib4/commit/669ad32efca36c9727c06f7c721856e86bd58006 because @Eric Wieser mentioned me in a commit which is now part of the master mainline and people periodically rebase this commit onto feature branches

[Mario Carneiro]

I'm pretty sure every occurrence of this is a mistake, and the resulting branches end up having hundreds of commits

[Ruben Van de Velde]

Suggestion: don't mention people by user name in commit messages :innocent: