How I fetched, edited, and merged Ville's PR #4618

[Edward K. Ream]

I have just merged Ville's PR #4618. Here is the workflow I used, from the second answer to this stack overflow question:

Note: The URLs shown below do not use the git: prefix. I think that was a typo.

Grabbing their commits

git fetch /path/to/coworkers/repo.git theirbranch:ournameforbranch

This creates a local branch named ournameforbranch which is exactly the same as what theirbranch was for them. For the question example, the last argument would be foo:foo.

Pushing it back

Oftentimes, you want to fix something of theirs and push it right back. That's possible too: 

git push /path/to/coworkers/repo.git  ournameforbranch

My actual URLS

The first PR I merged was in this branch: vv-colorizer-skip-trace-by-default

To fetch

git fetch https://github.com/vivainio/leo-editor.git vv-colorizer-skip-trace-by-default:vv-colorizer-skip-trace-by-default

To push

git push https://github.com/vivainio/leo-editor.git vv-colorizer-skip-trace-by-default

HTH. I'm a newbie to all this. All comments and corrections are welcome.

Edward