backporting.md

This is one possible flow for backporting fixes to old branches.

Let's say we want to backport commit f54200217d57c64bdeac93192aa3ff9fc53d5890 to branch DistR-1_0_x.

First we create a local Distr-1_0_x branch:

$ git checkout -b DistR-1_0_x remotes/origin/DistR-1_0_x

Then we backport the commit with git cherry-pick:

$ git cherry-pick f54200217d57c64bdeac93192aa3ff9fc53d5890

Finally we commit the changes and push to the repo:

$ git commit -a
$ git push