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: May 02 2025 at 03:31 UTC