From a89c8e8aea5767be7036b5348a5116427f57630c Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Wed, 20 Nov 2024 11:53:42 -0500 Subject: [PATCH] fix: Readme.md needs "git" token in lakefile.lean --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2873f65536..e20b87c09f 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ The "batteries included" extended library for Lean 4. This is a collection of da To use `batteries` in your project, add the following to your `lakefile.lean`: ```lean -require "leanprover-community" / "batteries" @ "main" +require "leanprover-community" / "batteries" @ git "main" ``` Or add the following to your `lakefile.toml`: ```toml