Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

-time should understand multibyte encodings #3659

Closed
coqbot opened this issue Sep 24, 2014 · 5 comments
Closed

-time should understand multibyte encodings #3659

coqbot opened this issue Sep 24, 2014 · 5 comments

Comments

@coqbot
Copy link
Contributor

coqbot commented Sep 24, 2014

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3659
From: @mikeshulman
Reported version: trunk
CC: @JasonGross, @ppedrot

@coqbot
Copy link
Contributor Author

coqbot commented Sep 24, 2014

Comment author: @mikeshulman

It appears that the snippets of code shown by the output of -time are simply a fixed number of bytes. If the cutoff happens to come in the middle of a multibyte character, weirdness ensues.

@coqbot
Copy link
Contributor Author

coqbot commented Sep 26, 2014

Comment author: @ppedrot

That's not difficult to fix if we know what encoding we are expecting. Nonetheless, I am unsure about the fact that Coq's one encoding is or should be UTF-8.

@coqbot
Copy link
Contributor Author

coqbot commented Sep 26, 2014

Comment author: @JasonGross

Is there any reason for picking a non-ASCII default encoding other than UTF-8?

@coqbot
Copy link
Contributor Author

coqbot commented Sep 26, 2014

Comment author: @mikeshulman

What about using the OS default system encoding?

@coqbot
Copy link
Contributor Author

coqbot commented May 4, 2017

Comment author: @ppedrot

See #609.

@coqbot coqbot closed this as completed Jun 9, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant