Zulip Chat Archive

Stream: new members

Topic: Windows clone project error

Logan Murphy (Feb 23 2022 at 17:27):

Any idea what how to resolve this error when trying to clone a Lean project on windows? windows_err.png

Yakov Pechersky (Feb 23 2022 at 17:43):

Your git config is borked. Run this: git config --core.autocrlf input

Last updated: May 02 2025 at 03:31 UTC