diff options
| author | Robert Norton | 2018-05-10 17:40:48 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-10 17:40:48 +0100 |
| commit | 6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d (patch) | |
| tree | 393b217b376022500b1bfc5ec73f53da30722962 /src | |
| parent | 938f06bc6c711ef3e777beaace7da8d4aee158b9 (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.ml | 2 |
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 |
