Zulip Chat Archive

Stream: new members

Topic: GitHub advice


Felix Weilacher (Dec 23 2022 at 17:57):

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 (Dec 23 2022 at 18:00):

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


Last updated: Dec 20 2023 at 11:08 UTC