Hm, I seem to be able to copy and paste the mus produced by pdflatex or by using pandoc to convert from LaTeX to HTML. Perhaps they're using something bespoke.