Zulip Chat Archive
Stream: new members
Topic: Failure to read file
Daniyal Hameedi (Jul 08 2023 at 10:29):
Receiving the following error message in my lakefile.lean file in a project:
Capture.PNG
I've had a look at the file in question and it is in the specified directory but has nothing in it.
Last updated: Dec 20 2023 at 11:08 UTC