Stream: Coq devs & plugin devs

Topic: XML protocol failure location


view this post on Zulip Hugo Herbelin (May 17 2024 at 10:02):

Finally, I found the reason for the bad location reporting using unicode in the xml protocol (thus e.g. in CoqIDE): there was a remaining place where line numbers were not serialized. I'm going to make a PR.


Last updated: Oct 13 2024 at 01:02 UTC