aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJim Fehrle2019-05-12 17:44:04 -0700
committerJim Fehrle2019-05-13 11:07:48 -0700
commit5e1238260c32227f8568fb1328f922cdeaa8dfc8 (patch)
tree6d21045fc8826d75580d4f06dc79ef6d76bac094
parent9f11eeefc204bdad029b66f30bc6c52377af63ae (diff)
Handle tags shorter than "diff." without an exception
-rw-r--r--vernac/topfmt.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 118c126970..bf2efb2542 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -201,7 +201,7 @@ let set_emacs_print_strings () =
let diff = "diff." in
List.iter (fun b ->
let (name, attrs) = b in
- if diff = (String.sub name 0 (String.length diff)) then
+ if CString.is_sub diff name 0 then
tag_map := CString.Map.add name
{ attrs with prefix = Some (Printf.sprintf "<%s>" name);
suffix = Some (Printf.sprintf "</%s>" name) }