[isabelle-dev] Jenkins maintenance window

[Jasmin Blanchette]

Hi Lars,

> However, turns out that the actual problem was that somebody pushed
> something completely unrelated (maybe a different repository?) into
> testboard. This also generated a gargantuan changelog in Jenkins. I
> don't blame that person, it could happen to anyone. But we need to fix
> this workflow of force-pushing into some "dumping ground" repository.
> Any ideas?

Was it me? I think I saw a warning to that effect, but with "-f" (which is necessary since we're creating new heads) it's too late once the warning is shown. I can easily change the trusty old script I use to push to testboard to make sure I do it from my Isabelle repository. If it happens once every five years or so, maybe it's not so great an issue that the workflow needs to be changed.

Jasmin