Zulip Chat Archive
Stream: new members
Topic: package configuration '.\lakefile.lean' has errors
Eric Wieser (Jul 08 2022 at 12:05):
I've moved this to a new topic; the previous question was by a different user, Kevin
Last updated: Dec 20 2023 at 11:08 UTC