Am 24.02.2012 um 09:16 schrieb Lukas Bulwahn:
> 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.
There's a much easier solution. Write a little script called "tb" that looks
like this:
(cd ~/isabelle; hg push -f testboard)
Then you'll never need to pass "-f" again in your life. No need for fancy hooks
or anything.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
