From 6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 10 May 2018 17:40:48 +0100
Subject: 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.

---
 src/latex.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

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
-- 
cgit v1.2.3