So… which is preferable? Should people export TeXmacs documents to HTML or rely on Mozilla’s PDF.js?
It depends on your motivation. This plugin is simply used to display PDF files in browsers. If you use TeXmacs to build a webpage, of course you want to export it as