diff options
| author | Maxime Dénès | 2017-05-09 09:04:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-09 09:04:13 +0200 |
| commit | c92e6ac43d2048d0f29e944177e946795b8b7fbf (patch) | |
| tree | dcaaf6e95686245178d1723b32a13dce54cfe408 | |
| parent | 398e64567386656f8c20b75cccff6ea4805dbd79 (diff) | |
| parent | 787a2c911b88bff399b37bfa8e11c0f1acecc6cd (diff) | |
Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |