From 5e1238260c32227f8568fb1328f922cdeaa8dfc8 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 12 May 2019 17:44:04 -0700
Subject: Handle tags shorter than "diff." without an exception

---
 vernac/topfmt.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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