[isabelle-dev] Small repository accident

[Makarius]

On Fri, 24 Feb 2012, Lukas Bulwahn wrote:

> On 02/24/2012 09:01 AM, Florian Haftmann wrote:
>> Accidentally I have pushed something into the main repository which was 
>> still supposed to be tested.  PLEASE IGNORE HEAD REVISION 0bd7c16a4200 and 
>> continue with the other head.
>> 
>> Sorry for this,
>>     Florian
>> 
>
> I was close to this mistake myself a couple of times already.
>
> It is the "evil" -f option with is now standard when pushing to the 
> testboard -- accidently pushing to the public repository (with -f) is 
> then done without checking as well.
>
> Isn't there a easy way to allow pushing to the testboard without writing 
> "-f" but still allowing to create new heads? Then we would never use the 
> -f option and cannot get into this trouble.

The hgrc file allows to specify default command line options for each 
command.  For example, I have harmless things like this in ~/.hgrc:

[defaults]
status = --color=always
diff = --color=always
log = -l 7 -v

It is also possible to have .hg/hgrc specific to individual repository 
clones.  So if testboard users are instructed to augment only that hgrc 
with the evil option once and for all, the problem of getting used to evil 
command lines in a different context is avoided.


 	Makarius