Push event web hooks should support Git push-options
Git supports push options, which are passed to the pre-receive and post-receive hooks in environment variables GIT_PUSH_OPTION_0, GIT_PUSH_OPTION_1, and so on. Gitlab should pass them through to the web hook in an array.
Proposal
When pushing a commit, a user can provide push options: git push -o 'foo' -o 'bar'
These should be available in the push event web hook:
{
"object_kind": "push",
...
"push_options": ["foo", "bar"]
}Documentation blurb
Gitlab supports push options in webhooks. These can be used to customize the treatment of pushes. For example, if there's a webhook that automatically creates or updates a MR on push, an option could indicate which users are listed as code reviewers, or automatically associate an issue id. If a webhook sends a message to an IRC channel, an option might specify which users to ping, or might indicate that no message should be sent.
To set options on a push, just add -o to your git push command. To use options in a webhook, look at the "push_options" array.