github not showing pushes

Stream: general

[Bolton Bailey]

Now that #8002 has all its dependencies, I've been trying to push new commits to it. But for some reason none of the commits I've pushed in the last hour or so are showing up on Github. Why might this be happening?

[Bolton Bailey]

Might it have something to do with the fact that this PR is for the prime-power-central-binom branch, rather than master? Why is this?

[Yaël Dillies]

I do see them here: https://github.com/leanprover-community/mathlib/commits/bertrand-2

[Bolton Bailey]

@Patrick Stevens should we change #8002 to be merging into master rather than this other branch?

[Patrick Stevens]

@Bolton Bailey Yes, certainly. This is an artefact of the Bors workflow; if we were just using "ordinary" GitHub squash-and-merge, that would have been automatic.

[Patrick Stevens]

I just fixed the base branch, your commits show up on the PR again

[Patrick Stevens]

(I used a different base branch because I wanted to see the diff as if the dependency branch had already gone into master, so I changed the PR to be into "my dependency branch" rather than master, so that the dependency diff didn't appear in the comparison because it was already in the base branch)

[Bolton Bailey]

Ah, cool