Zulip Chat Archive
Stream: mathlib4
Topic: Re-using a branch for a new PR?
Michael Stoll (Nov 11 2023 at 19:22):
Can I use a branch that was closed by bors because a PR was merged again for another PR?
Ruben Van de Velde (Nov 11 2023 at 19:28):
It will be a new branch with the same name, but sure
Last updated: May 02 2025 at 03:31 UTC