Add more git push options
This is a follow up to https://gitlab.com/gitlab-org/gitlab-ce/issues/43263 and https://gitlab.com/gitlab-org/gitlab-ce/merge_requests/26752 which added the following push options:
The new push options that would be useful on top of the above are:
I am asking for the above in behalf of @avar who is currently away.
I realized that there is already
-o ci.skip (see https://docs.gitlab.com/ee/ci/yaml/#skipping-jobs), so as far as I understand there is no need for
-o merge_this_right_away that was suggested.
This is related to: https://gitlab.com/gitlab-org/gitlab-ce/issues/5942