[isabelle-dev] Small repository accident

Lukas Bulwahn bulwahn at in.tum.de
Fri Feb 24 09:16:51 CET 2012

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.


More information about the isabelle-dev mailing list