Update README.md

lean-dojo · Dec 25, 2024 · d61040e · d61040e
1 parent 0129cc5
commit d61040e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -51,6 +51,10 @@ package «my-package» {
   ]
 }
 ```
+Alternatively, if your project uses lakefile.toml, you should have something like
+```
+moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
+```
 
 2. Add the following line to lakefile.lean, including the quotation marks:
 ```lean