Hello again, the generated HTML documentation makes automatically a call to the external mathjax javascript library. In debian this is considered a privacy breach, since cloudfare.com can see in its http server logs when someone has requested that library, probably with some associated information like the IP address, and a fingerprint of the browser. When a user locally installs an HTML documentation on his machine he can expect that this does not happen.
My question to you is: how useful is this library? I made a test and removed the mathjax lines, and I cannot see a difference. In that case I will just run an sed script that removes the lines when building the why3-doc-html package. BTW, I also tried switching it off in doc/conf.py, but that doesn't seem to have any effect. Thanks -Ralf. _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
