Git-Gui: Can the "push" button optionally be removed/disabled/hidden ?

Git-Gui: Can the "push" button optionally be removed/disabled/hidden ?

[Mirco Babin]

Dear Git Gui maintainers,

Is it possible to remove/hide/disable the push button via a
commandline parameter ? And if not currently possible, could such
functionality please be added ?

I have created an issue #73 -
https://github.com/prati0100/git-gui/issues/73 with extensive
information. But after reading the documentation on github it seems
this mailinglist should be used.

Kind Regards,
Mirco Babin

Re: Git-Gui: Can the "push" button optionally be removed/disabled/hidden ?

[Junio C Hamano]

Mirco Babin <mirco.babin@gmail.com> writes:

> Dear Git Gui maintainers,
>
> Is it possible to remove/hide/disable the push button via a
> commandline parameter ? And if not currently possible, could such
> functionality please be added ?

Just a comment from sideline; I am not involved or invested in
git-gui that much.

Why should "push" be so special?  Should other operations like
"pull", "stage", etc. that makes changes also optionally be hidden?
Where does this stop?

If "push" is not doing something useful for you, would there be a
way to make it more useful by allowing options that are not passed
to the underlying "git push" to be passed?

Thanks.