Feature request: warnings about languages not highlighted by the shipped script?

[favonia]

Hi, I wonder if odoc can give a warning about the language tags not supported by the shipped highlightjs script. An even better option might be vendoring files in https://github.com/highlightjs/cdn-release/tree/main/build/languages and ship exactly the scripts for languages used in the documentation, completely solving #951 and #953.

[Julow]

Shipping only the required languages is challenging as while Odoc outputs the support files (with the command odoc support-files) it doesn't consider the documentation that have been built.

Emitting a warning is possible but I'm not sure it's a good solution as the driver (odig, dune, ocaml.org) is free to ship a different highlightjs.js.

Perhaps odoc support-files could take a list of the required language highlightings as an argument ? But I'm not sure how/if that would be used by drivers.

If you are publishing your own documentation, providing your own highlightjs.js is the only short term solution that I see.