merging

Stream: mathlib4

[Scott Morrison]

@Patrick Massot, when I've been merging mathlib4 porting PRs, I've been editing the #port-status wiki to change Yes to No at the same time. I noticed you didn't do this on https://github.com/leanprover-community/mathlib4/pull/996, so this is the friendly reminder that it is helpful to do so. :-)

Hopefully soon this step won't be needed, in any case.

[Patrick Massot]

Should I do that as soon as I tell bors to merge? I was waiting for the actual merge (but then I went to do something else of course)

[Chris Hughes]

I haven't been doing that either. What do I have to do?

[Johan Commelin]

Update https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status from No to Yes

[Johan Commelin]

Hopefully this won't be needed anymore in 2 or 3 days.

[Scott Morrison]

I've been doing it as soon as I hit merge. I found that I have fewer accidents where I forget to follow up that way.

[Chris Hughes]

I haven't been doing that. Do I need to go back and do this to all the PRs I've merged?

[Scott Morrison]

Probably? I've caught some, but mostly only when they appear on the high priority graphs.

[Scott Morrison]

If we look at the output of scripts/port_status.py, and look for PR numbers that have already been closed, that should identify any that have slipped through like this.