[isabelle-dev] Small repository accident

[Lukas Bulwahn]

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.

Lukas