HOWTORELEASE.md

Instructions for publishing release

1. Create release on GitHub. Name git tag like "v1.x".
2. Run cd tools && ./docs-push-gh-pages.
3. Run cd tools && ./docker-push.