matching a non-merged mathlib3 PR

Stream: mathlib4

[Kevin Buzzard]

Am I right in thinking that we don't really want to review mathlib4 PRs made with a matching mathlib3 PR which is still open? (in case e.g. it doesn't get merged, or it only gets merged after more changes). Furthermore am I right in thinking that it's not even possible to make the complete mathlib4 PR until after the mathlib3 PR is merged, because we need a commit number and mathlib3 squash-merges stuff? I was just going through #queue4 and I found a couple of mathlib4 PRs with a corresponding unmerged mathlib3 PR.

[Yaël Dillies]

I am probably guilty for most of them, sorry :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

In fact you were guilty of 0 of them.