No means to specify push-options

[priitliivak]

Currently PushOp does not contain configuration for setting jGit push-options.
I tried using configuration value push.pushOption but Git documentation seems to indicate that config value is used only when command line parameter is missing

When no --push-option= is given from the command line, the values of configuration variable push.pushOption are used instead.

Enabling debug logs revealed that jGit is passing "push-options agent=git/2.18.1" to Git and thus configuration values are not used.

Did not find any ways how to set push-options at the moment.

[ajoberstar]

Looks like we could a pushOptions list to correspond to JGit's setPushOptions.

If that would solve your issue let me know. And if you have time to submit a PR, that would be much appreciated, otherwise this will wait until I have time to do another around of updates.