force push to gitlab
Created by: bernt-matthias
If I get it right the last sync created a merge commit at hzdr which we did not have here at github.
So one option might be to have a pull after the push(es) in the action. The alternative (implemented here) is to force push which definitely overwrites everything at hzdr.
Not sure if we need both pushes ..
--tags
All refs under refs/tags are pushed, in addition to refspecs explicitly listed on the command line.