Smaller suggestions can also be made through the github web interface as part of the pullrequest review, see https://egghead.io/lessons/github-add-suggestions-in-a-github-pr-review and https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/reviewing-changes-in-pull-requests/incorporating-feedback-in-your-pull-request
On Wednesday, 14 September 2022 at 04:15:10 UTC+2 Nils Bruin 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. 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. > > 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/a1ee452c-4706-4871-a6e3-092fae4119f0n%40googlegroups.com.
