diff options
| author | Jim Fehrle | 2019-05-12 17:44:04 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-05-13 11:07:48 -0700 |
| commit | 5e1238260c32227f8568fb1328f922cdeaa8dfc8 (patch) | |
| tree | 6d21045fc8826d75580d4f06dc79ef6d76bac094 | |
| parent | 9f11eeefc204bdad029b66f30bc6c52377af63ae (diff) | |
Handle tags shorter than "diff." without an exception
| -rw-r--r-- | vernac/topfmt.ml | 2 |
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) } |
