summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
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