On Wednesday, 22 January 2025 at 20:30:46 UTC-8 jackson...@gmail.com wrote:
I had a similar thought but didn’t know if it was possible. I don’t really understand the idea of being religious about not touching someone’s PR if they were the one that opened it. Surely just getting the code finished and merged is more important, and being able to rebase rather than abandoning seems like a good idea. The conversation on the PR is part of the sagemath repo, so team members can for the most part comment there. The code, however, resides in a fork that is owned by the person who made the PR. You can't really expect to be able to push updates to that branch. "Taking over" a PR on trac meant one would connect a different branch to the ticket. I'm not sure github allows that. It looks like "allow edits by maintainers" goes some way to alleviating these problems (see https://github.blog/news-insights/product-news/improving-collaboration-with-forks/), but I expect we don't have enough "maintainers" to really make this useful (only people with push privilege on the sagemath repo would qualify). If you'd know beforehand that there are several people who'll be working on a PR it should be possible to just make a fork where all these people are given push privilege. But that requires some advance planning which wouldn't help these after-the-fact resuscitation endeavours. There's always the option of forking the PR branch and make a new pull request from that. The git metadata would still accurately reflect authorship of the earlier commits. It would lead to a discontinuity in the discussion history, though, and it could give people the feeling their "PR" was stolen if they're more concentrated on PR authorship than commit authorship. For posterity, the git commit data is much more important but in github the PR discussions are much more visible, so it's not unlikely people would feel strongly about PR authorship. Even on trac, where tickets were owned by the organization, people would often feel attached to "their" tickets. -- 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 visit https://groups.google.com/d/msgid/sage-devel/b692ab88-53e4-4725-873c-1e2969c50c28n%40googlegroups.com.
