From dfbe9387054e2972449de7bf346059d3609529fa Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Fri, 29 Nov 2024 02:12:39 -0500 Subject: [PATCH] fix: dependency syntax for a reservoir+git lakefile.toml (#1067) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index e20b87c09f..36d46eee4d 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Or add the following to your `lakefile.toml`: [[require]] name = "batteries" scope = "leanprover-community" -version = "main" +rev = "main" ``` Additionally, please make sure that you're using the version of Lean that the current version of `batteries` expects. The easiest way to do this is to copy the [`lean-toolchain`](./lean-toolchain) file from this repository to your project. Once you've added the dependency declaration, the command `lake update` checks out the current version of `batteries` and writes it the Lake manifest file. Don't run this command again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest.