Some small github integration scripts

Update, 2018-04-01: I added git-remote-add-github, a tool for adding github forks as remotes.

This is a little script I cooked up a few months ago, then hacked on a little bit this week. It provides a convenient shortcut to locally fetch or merge the changes in a github pull request. It doesn't require any special privileges (e.g., github account, API key) to use, unlike other alternatives like github-cli (ghi).

Files currently attached to this page:

git-merge-pr	2.9kB
git-remote-add-github	1.8kB

# Quick commandline tool for fetching and/or merging github pull requests.
#
# Steps for use:
# 
# Once per computer or user, depending on location:
#     Install the program `jq`; debian package name `jq`
#
#     Place this in the system directory shown by `git --exec-path` or in any
#     directory listed on your $PATH, typically including $HOME/bin
#
#     You can (re)name it what you like, except that the name must begin
#     "git-".  If the script name includes "pull" or "merge", invoking it will
#     do a merge.  Otherwise, it will do a "fetch", leaving the branch for you
#     to inspect at FETCH_HEAD
#
#     (you can create the second copy with e.g. `ln -s`)
#
# Once for each clone:
#     Configure the github project, e.g.,
#         git config github.project linuxcnc/linuxcnc
# 
# To merge or fetch an individual pull request, just specify it by number:
#     git merge-pr 144
#
# If you put a copy / symlink as git-fetch-pr, you can also
#     git fetch-pr 144
#
# To act on a pull request associatred with another fork of this project,
# specify the name of the fork:
#
#     git fetch-pr jepler/linuxcnc#37
#
# This script does NOT check that you are merging the pull request to the
# branch requested on github.
#
# License: CC0 https://creativecommons.org/share-your-work/public-domain/cc0/
#          Also commonly called "Public Domain"