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: Dec 20 2023 at 11:08 UTC