On 17/01/2019 21:54, Makarius wrote: > > The problem behind this: Angeliki got administrative push-access to the > Isabelle repository, without anybody at Cambridge showing her how to use it. > > There is of course README_REPOSITORY, but the text is long. Here is the > ultra-short version: > > After every local commit, use "hg view" (or equivalent) to ensure that > the change is really what you want to make eternal when pushed to public.
Here is another (minor) error by Angeliki: 6b8d78186947 is actually a merge (a clean one according to "hg view"), but the log message makes it appear like a regular change. (README_REPOSITORY explains proper treatment of merge nodes.) I've seen that incident already on Monday -- still with a high temperature, and not in proper shape to look more closely or write private mails etc. Instead, I was watching silly things like https://www.youtube.com/watch?v=FOJtmDYcFMg -- not totally unrelated to this thread. Maybe Larry can show Angeliki how to operate the "hg" chainsaw adequately. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
