Re: [PATCH 4/4] Rename push.default to push.style
- From
- Santi Béjar <santi@agolina.net>
- Date
- Mar 30, 2009, 09:07 UTC
- Message-ID
- <adf1fd3d0903300207j479b6e91gc6ed00695a00e157@mail.gmail.com>
- In-Reply-To
- <adf1fd3d0903300200v65393b1bif0050392aa44652e@mail.gmail.com>
2009/3/30 Santi Béjar <santi@agolina.net>:
Show 10 quoted lines
> 2009/3/30 Johannes Schindelin <Johannes.Schindelin@gmx.de>: >> On Mon, 30 Mar 2009, Finn Arne Gangstad wrote: >>> Some people may have started setting push.default already, so changing >>> the name may cause additional grief. >> >> ... indeed, it is too late now. The milk has boiled already. > > I have it configured, but I think we can fix these type of things > while they are in 'next'. >
Now that I've recheck it, it seems to be in 'master', it's less clear, but I still think we can fix these type of things while they are not in a relased version.
The people with that setting is following the development version, and can easily notice/change it.
Santi