[isabelle-dev] Small repository accident
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri Feb 24 11:00:02 CET 2012
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.
More information about the isabelle-dev