I installed Agda and Im using VSC to load files, but I have an error when I try to load a saved file. The file open and displays correctly, but when I load it seems that some unicode characters conver to “?”. Before loading file:
After loading file:
I installed Agda and Im using VSC to load files, but I have an error when I try to load a saved file. The file open and displays correctly, but when I load it seems that some unicode characters conver to “?”. Before loading file:
After loading file:
See answer here stackoverflow.com/questions/30082741/… except select “Reopen with encoding” instead of save
Does this answer your question? Change the encoding of a file in Visual Studio Code
No, that didn’t work, I was using UTF-8 already, and I’m still seeing the same ?? symbols after reloading with UTF-8 (which has always been the default option).
Interestingly, when I open the text file in Notepad++, it displays correctly. So it looks like a bug in visual studio code?
I can bet you $10 right now that notepad detects another encoding. You’re very quick jumping to conclusion it’s a bug in extremely popular software. It almost never is.