max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: fixing path of the generated binary in documentation (#3093)

Browse source 
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)
This commit is contained in:
lu-bulhoes 2023-12-19 14:26:55 -03:00 • committed by GitHub
parent 67bfa19ce0
commit 312ea12bc2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/setup.md
View file

@ -50,10 +50,10 @@ Foo.lean # main file, import via `import Foo`
Foo/
A.lean # further files, import via e.g. `import Foo.A`
A/... # further nesting
build/ # `lake` build output directory
.lake/ # `lake` build output directory
```
After running `lake build` you will see a binary named `./build/bin/foo` and when you run it you should see the output:
After running `lake build` you will see a binary named `./.lake/build/bin/foo` and when you run it you should see the output:
```
Hello, world!
```