Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Wrong path in 2.4 "Meow!" #153

Open
lunaticabs opened this issue Mar 15, 2024 · 1 comment
Open

Wrong path in 2.4 "Meow!" #153

lunaticabs opened this issue Mar 15, 2024 · 1 comment

Comments

@lunaticabs
Copy link

Please quote the text that is incorrect:

echo "It works!" | ./build/bin/feline

In what way is this incorrect?

The path in here should be ./.lake/build/bin/feline. Because the current path should be in root directory in a project folder in general.

@david-christiansen
Copy link
Collaborator

The book is currently targeting a version of Lean that's a couple of months old. But this will indeed need fixing the next time I update it to the current version (which needs doing soon, much has changed!).

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants