From f7a858c0decdd6d1b0506c1be45e9bee08f3fcdb Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 14 Jun 2021 01:08:35 -0400 Subject: [PATCH] Add search path heading to README --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 9397799104..a37598bc9a 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,8 @@ On Windows (MSYS2): $ leanpkg build bin LINK_OPTS=-Wl,--export-all ``` +### Correcting Lake's Search Path + When running the built executable, you may need to ensure that `LEAN_PATH` includes the build directory of Lake (for Lake's `.olean` files) and Lean's library directory for stdlib's (ex., `Init`'s) `.olean` files. For example: