Add push options to the mike deploy command

[gusmb]

It would be nice to specify push options when pushing to the remote branch while deploying. A use case is to use
the "ci.skip" option to instruct Gitlab to skip the CI for the docs branch pushed by the mike deploy command....

https://docs.gitlab.com/ee/user/project/push_options.html

In my case I always see an ugly failed pipeline as non-existing for the docs branch since our Gitlab Server enforces the run of a pipeline.
There might be other use cases for push options.

[jimporter]

The -p/--push option is just a shorthand for the common case of running git push origin gh-pages after finishing everything else. I think all you should need to do is:

mike deploy
git push origin gh-pages --push-option=HELLO

[gusmb]

That works as well, I was just hoping that this could be handled natively with the mike CLI when using that shorthand as it is a common thing, instead of having to use the git CLI. I tried and it works but seems a bit redundant as I now need to give the remote to both mike and GIT. Pushing to origin fails from the pipeline as I need to set the correct access token

[jimporter]

I'd prefer to avoid adding more options to mike unless absolutely necessary. When it comes to doing non-default things with Git, I think it would be best to write the exact Git command so that it's maximally explicit. That way there's no confusion about what's really getting executed.

I guess I could see adding an option that forwards arbitrary args to subcommands, so that you could do mike deploy -X,--push-option=HELLO. I'm not sure though, since I think the explicit Git command makes it more obvious what's happening.

[gusmb]

Fair enough. I guess in that case documentation examples around use cases like the push option to skip the CI etc, would be good so it's clear when to skip the -p option and handle the git separately with git CLI. The example you gave me earlier was helpful and worked for me with minor tweaks.

[jimporter]

One thing I've been considering here is that it's probably worth adding support for some set of environment variables to control Git behavior. For example, a user might want to use a specific version of Git not in their path, and so would set GIT=/path/to/git. Similarly, we could support this issue via a GIT_PUSH_FLAGS variable. Then there would be similar env vars for each other Git subcommand we use. I'm not sure how useful that is, but it would be the most general-purpose solution to the problem...

[gusmb]

Yeah seems like adding support for git options so that the user can consolidate the docs version management with just the mike CLI instead of part with mike and part with git would help keep things more tidy