You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In the Lean Manual, section "Extended Setup Notes", we have the path of builded binary pointed to "./build/bin/foo" but this is an incorrect path. The generated binary stay in "./lake/build/bin/foo".
User Experience: This feature can help new lean users to better understand the setup environment.
Beneficiaries: beginners
Maintainability: No
Community Feedback
Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered:
This PR fixes the documentation error in "Extended Setup Notes", where
the path of builded binary is pointed to
`./build/bin/foo`, but the truly path is `./lake/build/bin/foo`.
---
Closes#3094 (`RFC` or `bug` issue number fixed by this PR, if any)
Proposal
In the Lean Manual, section "Extended Setup Notes", we have the path of builded binary pointed to "./build/bin/foo" but this is an incorrect path. The generated binary stay in "./lake/build/bin/foo".
User Experience: This feature can help new lean users to better understand the setup environment.
Beneficiaries: beginners
Maintainability: No
Community Feedback
Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: