Skip to content

Commit 9b912c9

Browse files
authored
fix: include reference text in TeX output (#917)
Includes the link text in references along with the page number, using a `\hyperref` tag instead of `\autoref`. Closes #915
1 parent 74fc8d1 commit 9b912c9

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/verso-manual/VersoManual.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
118118
else
119119
-- Intra-document links should be page references
120120
let label := labelForTeX dest.htmlId
121-
pure \TeX{\autoref{\Lean{label}}" (p."~\pageref{\Lean{label}} ")"}
121+
pure \TeX{\hyperref[\Lean{label}]{\Lean{← content.mapM go}}" (p."~\pageref{\Lean{label}} ")"}
122122

123123
toHtml :=
124124
open Verso.Output.Html in

0 commit comments

Comments
 (0)