Re: [PATCH v3 0/9] User manual updates

I've taken the following to 'maint', some with minor and obvious
fix-ups:

  user-manual: use 'remote add' to setup push URLs
  user-manual: give 'git push -f' as an alternative to +master
  user-manual: mention 'git remote add' for remote branch config
  user-manual: use 'git config --global user.*' for setup
  user-manual: use -o latest.tar.gz to create a gzipped tarball

I think I've sent reviews for all others, except for the `backtick`
one.  I think it is more efficient to do that one _after_ we are
done with all the others.

Thanks.