Skip to content

KaTeX headers are missing for documentation pages. #1092

@gadmm

Description

@gadmm

The KaTeX <link> and <style> headers seem to be missing in html files generated from mld files.

Example input mld file:

{0 Math}

Here is some math {m 4^{-10}}.

Generated html:

<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>math (math)</title><meta charset="utf-8"/><link rel="stylesheet" href="odoc.css"/><meta name="generator" content="odoc 2.4.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><header class="odoc-preamble"><h1 id="math"><a href="#math" class="anchor"></a>Math</h1><p>Here is some math <code class="odoc-katex-math">4^{-10}</code>.</p></header><div class="odoc-content"></div></body></html>

(missing the katex js script & so on).

The KaTeX <link> and <style> headers are correctly present in documentation for the mli files in the same project.

I am using odoc 2.4.1.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions