From 7055f953f1e02cceb5e252e6f4c8724fc565a81a Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 2 Feb 2023 15:40:02 -0500 Subject: [PATCH] doc: fix typo closes leanprover/lake#151 --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 4b8dcf60fb..99a642e974 100644 --- a/README.md +++ b/README.md @@ -371,7 +371,7 @@ Thank Anders Christiansen Sørby ([@Anderssorby](https://github.com/Anderssorby) ### Augmenting Lake's Search Path -The `lake` executable needs to know where to find the Lean library files (e.g., `.olean`. `.ilean`) for the modules used in the package configuration file (and their source files for go-to-definition support in the editor). Lake will intelligently setup an initial search path based on the location of its own executable and `lean`. +The `lake` executable needs to know where to find the Lean library files (e.g., `.olean`, `.ilean`) for the modules used in the package configuration file (and their source files for go-to-definition support in the editor). Lake will intelligently setup an initial search path based on the location of its own executable and `lean`. Specifically, if Lake is co-located with `lean` (i.e., there is `lean` executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located under their shared sysroot. In particular, their binaries are located in `/bin`, their Lean libraries in `/lib/lean`, Lean's source files in `/src/lean`, and Lake's source files in `/src/lean/lake`. Otherwise, it will run `lean --print-prefix` to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that `lake` is at `/build/bin/lake` with its Lean libraries at `/build/lib` and its sources in directly in ``.