I don't understand how to tag a version properly in git so the version is pushed to github together with the tag.
In fact I don't even know which is the right moment for setting the the tag name.
Do I need to set the tag before the local commit or after the local commit?
I've seriously checked the git documentation.
And then, when I want to push to remote i.e. github do I explicitly need to set the tag name again like in this example:
https://stackoverflow.com/a/5195913/716568
Is there no way to automatically push in sync with the currently set local tag?
The right moment for setting tag name is when you create the tag. And you can create and push it at any time. You can create a tag immediately after commit or a week later. Up to you.
When you want to push tag(s) with commits either you name the tags in the command line (git push origin master tag v3.42, for example) or you can add push.followTags=true to config: git config [--global] push.followTags true ([--global] means optional — you have to decide if you want the settings in your global config (per-user) file or local (per repo)); with this setting git pushes tags when it pushes commits pointed to by these tags.
You may push a tag alone: git push origin tag v3.42. Git will push the tag and all commits required to complete the branch.