GitHub advice

Stream: new members

[Felix Weilacher]

Are we meant to create a new branch of mathlib for each PR? It seems annoying to do so, but if I use the same branch for two PRs in a row, the latter one still seems to display the changes from the first one, even if that first one has been merged.

[Riccardo Brasca]

Branch are very cheap, so yes, the usual procedure is to create a new branch for each PR.