On 14.08.2012 20:12, Tjark Weber wrote: > If these files are intentionally generated in isabelle/.../ and not > meant to be under version control, I am not sure I see the abuse in > adding them to .hgignore. On the other hand, if they are a mess and an > issue, perhaps that could be addressed. > > Anyway, what do you do to keep the output of "hg status" uncluttered?
If the .hgignore in the repository stays at it is, you can add your own private ignore file; see hgignore(5).
-- Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
