Add option to skip CI when pull mirroring

Problem to solve

Presently the repository mirroring option (auto-push) does not allow specification of --push-options. It would be nice to have this.

Intended users

Unknown

Further details

One application of this is when using repository mirroring to push to another GitLab repository. It would then be nice to have the option of avoiding triggering the CI pipelines. This is useful e.g. if the target repository does not allow the same runners as the source repository. Skipping the CI pipelines can be accomplished using --push-options ci.skip as documented here

Proposal

Add a field push options in the repository mirroring settings. The user can then use this field to set custom push options.

Documentation

Testing

What does success look like, and how can we measure that?

Links / references