search

leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

fix(library/module_mgr): ignore '\r' changes #1986

Closed gebner closed 5 years ago

gebner commented 5 years ago

(As reported and complained about by @digama0, @ChrisHughes24, @kckennylau in Amsterdam.)

Apparently, on windows vscode changes the line-endings of a file when sending it to the server (as compared to the on-disk copy). This seems to happen when the on-disk file has CR-LF endings. Then the server thinks the file has changed and will recompile everything.

As a workaround, we just ignore CR when checking whether a file is changed. (This doesn't affect command-line usage, which depends on timestamps.)

gebner commented 5 years ago

(We've tested this workaround on @robertylewis's laptop and it works.)

kckennylau commented 5 years ago

I second this PR.