Hi Clemens, > Please let me know if you need to make changes to locales.ML. I want to > make sure that routes out of certain quirks there don't get blocked > accidentally.
the only change to locales.ML in the pipeline is http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5 and I do not forsee anything else in that respect. If it comes to happen nonetheless, I will exhibit that change similarly before pushing it to any main upstream. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
