Release process: add a git push

This can be useful e.g. when 2 RMs share the work, to ensure
the work done by the first one is actually pushed somewhere
the second one will find it.