Sorry, I’m to blame for this. When Angeliki mentioned she had merge conflicts, it turned out she didn’t have diffmerge (or anything similar) on her machine. By the time I got everything configured and managed to resolve the conflicts (largely by discarding her work unfortunately), I unthinkingly pushed the result without testing.
Larry > On 18 Jan 2019, at 10:42, Lars Hupel <hu...@in.tum.de> wrote: > >> The problem behind this: Angeliki got administrative push-access to the >> Isabelle repository, without anybody at Cambridge showing her how to use it. > > Before we start blaming individual people, this is not a person problem, > but a tooling problem. Industry has figured out this problem years ago. > One doesn't simply allow pushes to master (or "default" in Mercurial). > CakeML has adopted this too. > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
