From 312ea12bc2e5c679810a2afcd3dd9e73ea5c69f9 Mon Sep 17 00:00:00 2001
From: lu-bulhoes <153877324+lu-bulhoes@users.noreply.github.com>
Date: Tue, 19 Dec 2023 14:26:55 -0300
Subject: [PATCH] fix: fixing path of the generated binary in documentation
 (#3093)

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)
---
 doc/setup.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/setup.md b/doc/setup.md
index 12b24179cf..579bdd93e7 100644
--- a/doc/setup.md
+++ b/doc/setup.md
@@ -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!
 ```