summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorRobert Norton2018-05-10 17:40:48 +0100
committerRobert Norton2018-05-10 17:40:48 +0100
commit6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d (patch)
tree393b217b376022500b1bfc5ec73f53da30722962 /src
parent938f06bc6c711ef3e777beaace7da8d4aee158b9 (diff)
latex: don't include the prefix in the label. This means we have the option of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels.
Diffstat (limited to 'src')
-rw-r--r--src/latex.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/latex.ml b/src/latex.ml
index f16dddd8..8688eaa8 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -123,7 +123,7 @@ let commands = ref StringSet.empty
let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l, _) as annot) =
let labelling = match label with
| None -> ""
- | Some l -> Printf.sprintf "\\label{%s%s}" prefix l
+ | Some l -> Printf.sprintf "\\label{%s}" l
in
let cmd = !opt_prefix_latex ^ prefix ^ cmd in
if StringSet.mem cmd !commands then