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

From: Junio C Hamano <[email-masked]>
Date: Thu, 27 Jan 2022 11:06:35 -0800

Mirco Babin <[email-masked]> 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.