On 24.02.2012 09:16, 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.
One could instead install a hook in the main repository which prevents
multiple heads via push:
http://mercurial.selenic.com/wiki/TipsAndTricks#Prevent_a_push_that_would_create_multiple_heads
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
