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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
