Stream: Coq devs & plugin devs

Topic: git prw: a command to easily fetch & force-push a PR branch

Erik Martin-Dorel (Apr 30 2021 at 22:37):

Dear Coq devs,
In case it'd be useful during some of your workflows, FYI I've just released two simple scripts git pr and git prw, which can be integrated in Git just like aliases.
The aim is just:

• for git pr 420 upstream:
  • fetch the last version of PR #420 from GH remote upstream and overwrite the "read-only" local branch named pr/420,
  • checkout pr/420;
• for git prw 420 upstream:
  • fetch the upstream branch likewise if pr/420 does not exist already (one can pass -f to always overwrite),
  • checkout pr/420,
  • and set its upstream branch to the appropriate branch from the remote GitHub fork repository associated to the PR.

(see this post for details)
HTH

Emilio Jesús Gallego Arias (Apr 30 2021 at 22:39):

Interesting @Erik Martin-Dorel , what is the difference with hub checkout PRURL? and variants ?

Erik Martin-Dorel (Apr 30 2021 at 22:48):

Hi @Emilio Jesús Gallego Arias, two main differences:

• one need not install the hub executable, git-pr is a simple Bash script that one can put in one's PATH;
• hub checkout and e.g. the alternative from tj/git-extras only implement the fetch of a read-only branch − very useful for reviewing indeed, but in practice one sometimes wants to (force)push somebody else's PR (either because the PR author is not responsive, or for pair-programming): this is only feasible by adding a remote manually, or using the feature from git prw

Théo Zimmermann (May 01 2021 at 08:14):

Great! I have personally been using gh pr, which is the official GitHub command line and has the same limitations as hub (very good for checking out a PR, but doesn't handle pushing back). But I noticed that I can still push without adding a remote, by passing the remote URL in the list of git push arguments.

Lasse Blaauwbroek (May 01 2021 at 14:16):

Note for Emacs users: With the Magit Forge plugin, you can also easily checkout a pull request. It also adds a new remote so that you can push. https://magit.vc/manual/forge/Branching.html#Branching

Erik Martin-Dorel (May 01 2021 at 15:23):

Hi @Lasse, as a Magit user (but not yet a Forge user :), thanks for sharing this tip!

Last updated: Sep 09 2024 at 04:02 UTC