Gabriel Hondet

This must be caused by the double `_` interpreted by the mathjax engine. Normally, the pretty printer [Logippedia](https://github.com/gabrielhdt/logippedia) should be run on these strings, which would escape the `_`. In...

So you want the pretty printer to be in the repository?

Ah all right, that's a good idea. I think we should 1. use an environment variable 2. use the command line flag so that if both are set, the command...

As far as I understand, this is needed by the hol light export (Emilie knows that better): it must be downloaded with hol light files. There should be a note...