On Wed, 14 Sep 2022, 03:15 Nils Bruin, <nbr...@sfu.ca> wrote: > On Tuesday, 13 September 2022 at 14:04:24 UTC-7 dim...@gmail.com wrote: > >> >> >> On Tue, 13 Sep 2022, 21:56 Nils Bruin, <nbr...@sfu.ca> wrote: >> >>> I'd actually be interested in knowing what the substitute for "git trac >>> checkout ..." is. Because with trac, all ticket branches are present in the >>> "trac" repository, you can pull anything from there. If I have to >>> merge/pull from developer branch, do I need to add another remote to my >>> local sage git repository? That sounds very laborious. Particularly for how >>> to keep it up-to-date. >>> >> >> No, you don't need to add the remote of the author of the PR, because the >> PR is a branch in the main repo. >> >> git-trac's functionality is provided by cli, a command line tool ftom >> GitHub, so this is all covered (except parts of git-trac only used by >> Volker-but you don't need to worry about this) >> >> it's explained in some detail in docs prepared by Matthias. >> >> Yes, indeed. "gh pr checkout" ( > https://cli.github.com/manual/gh_pr_checkout) looks like pretty much like > an exact analogue for "git trac checkout" > > 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. > > It's not clear to me yet what the github analogue of that would be ... I > guess a different "pr" could be tied to a given issue. > No, not really. The github analogue is to do a PR on the repo where the original PR came from, repo P, say. not sure whether gh allows an easy way to do so; with plain git you just push your changes onto your fork (which is just a different remote for your local git repo), and there, using web interface, create a PR - you have a choice of upstreams to send the PR to, so you choose the correct one, namely, repo P. Now, the owner of repo P approves/merges your PR, and the commits there are automatically added to the original PR (this is a "PR update"). to compare this with using plain git with trac, it's about the same complexity, there is extra step of approving/merging done by the owner of repo P (which is few clicks), but you don't need to mess with the new name for the branch on trac, it's a better web UI - and only the changes the the owner of repo P make its way into the original PR. It would be reasonable to expect that gh should facilitate this, I'm just not familiar with it. (maybe it is extendable?) But in that case, a direct analogue of "git trac" would focus on "issues", > and pull the currently registered "pr" for a given issue and tie my new > branch as a "pr" to that issue if I want to make a change to a ticket. > GitHub does not restrict you to one PR per issue, in this sense it is more flexible. You don't have to automatically close an issue by a PR, and anyway, the issue reporter can reopen it, it's not like trac tickets, which, once closed, can't be easily reopened. > Perhaps it's nice to address how to "make a friendly amendment" to someone > else's "pr" or "issue", or how to collaborate on tickets/issues/pr's . In > my work on trac tickets that happened quite a bit and "git trac > checkout/push" makes the workflow superconvenient for that. It would be > nice to have a convenient convention on how to replicate that on github. > > > -- > 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/e0a37229-9a65-40f5-aad0-106a42e6242fn%40googlegroups.com > <https://groups.google.com/d/msgid/sage-devel/e0a37229-9a65-40f5-aad0-106a42e6242fn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAAWYfq3c%2B06uyhKsaLANgHYbjGAcSuHkae7CcZo5wz-_z1mHUw%40mail.gmail.com.
