[isabelle-dev] Small repository accident

[Jasmin Christian Blanchette]

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