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