cli: git-merge

[tiborsimko]

Introduce git-merge command that would complement git-checkout command.

Its purpose is to merge a set of PRs to master and possibly to push

Example workflow:

The integrator checks a set of PR:

$ reana-dev git-checkout --fetch \
                         -b r-w-controller 401 \
                         -b r-j-controller 302 \

When everything is working, the integrator would like to merge some of them to master:

$ reana-dev git-merge -b r-w-controller 401 -b r-j-controller 302 [--push]

This command should do, for each given repo:

• git fetch upstream in given repositories to check whether local pr-401 branch is identical to upstream/pr/401 to prevent errors;
• if we are up to date, do git merge --ff-only upstream/pr/401 to master
• then delete locally checked out branch pr-401
• optionally, when --push argument is used, the new master branch should be pushed to upstream and origin;
• note that we already have git-push command which could be also amended for that effect (to add an option where to push, origin or upstream)

For example, I have been using the following alias:

merge-push-delete-pr = !sh -c 'git fetch upstream && git checkout master && git merge --ff-only upstream/master && git merge --ff-only upstream/pr/$1 && git branch -d pr-$1 && git push upstream master && git push origin master' -

The command would do something similar, but for a set of REANA components associated to a PR group.

Note: we could use simple git commands for now and investigate moving to gh command later (starting from git-fork and friends).