Mirco Babin <mirco.babin@xxxxxxxxx> 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.
