git: Add pull request fetching alias

Gets a pull request for the repo by directly fetching from the pull
folder of the repository. Works perfectly with github (should also work
with gitlab, and gitea/forgejo).

Searches for a remote called github or uses the default origin one.

vcs/git/config/git/config

@@ -28,6 +28,11 @@
   diffsyn       = "!git difftool --tool difftastic"                                # add syntax-driven diff using treesitter
   diffside      = "!DELTA_FEATURES='+side-by-side' git diff"                       # add side-by-side diffing
   delta         = "![ $TERM_DARK = false ] && delta --light || delta"              # Take care that we always display right color scheme
+
+  # check out a github PR directly on the commandline, creates pr/4 or pr/<number> branch locally
+  pr  = "!f() { git fetch -fu ${2:-$(git remote |grep ^github || echo origin)} refs/pull/$1/head:pr/$1 }; f"
+  # remove all pr/<number> local branches
+  pr-clean = "!git for-each-ref refs/heads/pr/* --format='%(refname)' | while read ref ; do branch=${ref#refs/heads/} ; git branch -D $branch ; done"
 [commit]
   gpgsign       = true                                                             # sign commits as me
   verbose       = true                                                             # Always show diff when preparing commit message