Make root dir required for lean more obvious

cedar-policy · Nov 13, 2024 · 8b2318b · 8b2318b
1 parent d0d8a21
commit 8b2318b
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/cedar-lean/README.md b/cedar-lean/README.md
@@ -12,6 +12,9 @@ Follow [these instructions](https://leanprover.github.io/lean4/doc/setup.html) t
 
 To use VS Code, open the `cedar-lean` folder as the root directory.
 
+> [!WARNING]
+> The VS Code Lean plugin _will not_ work properly if this project is opened with `cedar-spec` as the root.
+
 To build code and proofs from the command line:
 
 ```shell