doc: clarify which folder to run npm in (#367)

* Update dev.md lerna commands are outdated (and still not working) * Update docs/dev.md --------- Co-authored-by: Wojciech Nawrocki <[email protected]>
leanprover · Dec 7, 2023 · 9a70ded · 9a70ded
1 parent 940658e
commit 9a70ded
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docs/dev.md b/docs/dev.md
@@ -14,7 +14,7 @@ See the following design topics:
 
 ### Building
 - Make sure you have an up to date installation of `npm` and `node.js`.  For example `npm` version 8.1.3 and `node.js` version v16.13.0.
-- Run `npm install` in this folder. This installs the Lerna package manager.
+- Run `npm install` in your workspace root folder. This installs the Lerna package manager.
 - Run `npx lerna bootstrap`. This sets up the project's dependencies.
 - Run `npx lerna run build`. This compiles the extension (which is necessary for go-to-definition in VS Code).