[isabelle-dev] Small repository accident
bulwahn at in.tum.de
Fri Feb 24 09:16:51 CET 2012
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,
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.
More information about the isabelle-dev