diff options
| author | Pierre-Marie Pédrot | 2017-05-04 08:50:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-05 17:58:16 +0200 |
| commit | 787a2c911b88bff399b37bfa8e11c0f1acecc6cd (patch) | |
| tree | dcaaf6e95686245178d1723b32a13dce54cfe408 /API | |
| parent | 398e64567386656f8c20b75cccff6ea4805dbd79 (diff) | |
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.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions