I see that the secret lies in the difference between .hgrc and .hg/hgrc (how silly of me) Larry
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
