On Tuesday, September 13, 2022 at 7:15:10 PM UTC-7 Nils Bruin wrote: > What I was not able to find, though, was the equivalent of "git trac > push", which can sometimes be very convenient for making a small friendly > amendment to a proposed change. I would not expect to be able to push to > someone else's fork (I cannot push to someone else's branch on trac > anyway), but I can of course push to my own branch -- git-trac in that > situation pushes to a branch in my name and does the required magic to tie > that branch to the relevant ticket. >
One way to do this is using https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/working-with-forks/allowing-changes-to-a-pull-request-branch-created-from-a-fork This is a checkmark that the author of a PR can set or unset. -- 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/eee44d79-d7a6-44f6-8306-c7e7058e7b8cn%40googlegroups.com.
