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

Mirco Babin· Jan 27, 2022, 12:06 UTC · lore

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

Junio C Hamano· Jan 27, 2022, 19:06 UTC · re: Mirco Babin · lore

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

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

Show 5 quoted lines

> 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.