From 787a2c911b88bff399b37bfa8e11c0f1acecc6cd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 May 2017 08:50:27 +0200
Subject: Fix bug #3659: -time should understand multibyte encodings.

We assume Coq always outputs UTF-8 (is it really the case?) and cut strings
after 30 UTF-8 characters instead of using the standard String function.
---
 toplevel/vernac.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bfdae85d50..2a599444c2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -160,7 +160,9 @@ let pr_new_syntax po loc chan_beautify ocom =
    and a glimpse of the executed command *)
 
 let pp_cmd_header loc com =
-  let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
+  let shorten s =
+    if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+  in
   let noblank s =
     for i = 0 to String.length s - 1 do
       match s.[i] with
-- 
cgit v1.2.3