On 2022-06-09 02:23, Jason Hu wrote: > Another question on html: is there a hook to add custom js file > without resorting to external tools? I don't think so, but perhaps the option --html-highlight=code could be of use for you: https://agda.readthedocs.io/en/latest/tools/generating-html.html -- /NAD