From eec57bef3360eddf331370393ffc0afa3d7f01cf Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 17 Feb 2015 11:47:35 -0500 Subject: [PATCH] doc(syntax_highlight_in_latex.md): use bitbucket.org/leanprover/pygments-main [skip ci] --- doc/syntax_highlight_in_latex.md | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/doc/syntax_highlight_in_latex.md b/doc/syntax_highlight_in_latex.md index e5cc2e883..ebca50b21 100644 --- a/doc/syntax_highlight_in_latex.md +++ b/doc/syntax_highlight_in_latex.md @@ -1,20 +1,20 @@ -We provide a way to syntax-highlight Lean code in LaTeX documents. +We provide a way to syntax-highlight Lean code in LaTeX documents. It requires a Python package `Pygments` and a LaTeX package `minted`. Python Package: `Pygments` -------------------------- -Checkout [Pygments development repository][pygments-dev] and build Pygments: +Checkout [Leanprover's Pygments repository][lean-pygments] and build Pygments: ```bash -hg clone https://bitbucket.org/birkenfeld/pygments-main/ +hg clone https://bitbucket.org/leanprover/pygments-main cd pygments-main make mapfiles sudo ./setup.py install ```` -[pygments-dev]: https://bitbucket.org/birkenfeld/pygments-main +[lean-pygments]: https://bitbucket.org/leanprover/pygments-main LaTeX package: `minted` @@ -61,13 +61,11 @@ xelatex --shell-escape test Some remarks: - - `xelatex` is required to handle unicode in LaTeX. + - `xelatex` is required to handle unicode in LaTeX. - `--shell-escape` option is needed to allow `xelatex` to execute `pygmentize` in a shell. - + Contribute ---------- -Please fork [Leonardo de Moura's Pygments repository][pygments-lean], improve it, and make a pull-request. - -[pygments-lean]: https://bitbucket.org/leodemoura/pygments-main +Please fork [Leanprover's Pygments repository][lean-pygments], improve it, and make a pull-request.