From dd42a0919d92e5eb5440317d77f163e9296a290a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 11 Dec 2023 09:16:40 +0000 Subject: [PATCH] doc: explain how to use custom lexers in the latest minted (#3047) v3.0 is not yet released; in the meantime, the previous instructions did not work in the latest version without some hacks. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/XeLaTeX.20with.20minted.20error/near/406959183) --- doc/syntax_highlight_in_latex.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/doc/syntax_highlight_in_latex.md b/doc/syntax_highlight_in_latex.md index 572a441041..251fd5c3f8 100644 --- a/doc/syntax_highlight_in_latex.md +++ b/doc/syntax_highlight_in_latex.md @@ -67,6 +67,9 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f \end{document} ``` +If your version of `minted` is v2.7 or newer, but before v3.0, +you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360. + You can then compile `test.tex` by executing the following command: ```bash