On Friday, September 9, 2022 at 9:34:16 PM UTC-7 Travis Scrimshaw wrote: > I really dislike Github's decentralized approach with PR and having to > have separate clones of the repo within each user. My understanding is if > two people have different fixes, then they individually submit PRs that are > not explicitly linked with each other, much less with a specific bug report > issue.
In the PR you would include a comment such as "Fixes #1234", which links it to an Issue (bug report). Yes, there can be multiple competing PRs in order solve one ticket. Better than edit wars on a Trac ticket. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/2548301a-19d8-4ab5-ab1c-84f3fdcf5bbcn%40googlegroups.com.
