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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
