From: Santi Béjar <santi@agolina.net>
Date: Mon, 30 Mar 2009 09:07:10 GMT
Subject: Re: [PATCH 4/4] Rename push.default to push.style
Message-ID: <adf1fd3d0903300207j479b6e91gc6ed00695a00e157@mail.gmail.com>
In-Reply-To: <adf1fd3d0903300200v65393b1bif0050392aa44652e@mail.gmail.com>

2009/3/30 Santi Béjar <santi@agolina.net>:
> 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