try removing LeanCopilot?

ImperialCollegeLondon · Dec 14, 2023 · 1f16421 · 1f16421
1 parent ddb5ab1
commit 1f16421
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/lakefile.lean b/lakefile.lean
@@ -25,7 +25,6 @@ package FLT where
   moreServerArgs := moreServerArgs
 
 require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
-require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot" @ "v1.0.0"
 
 -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
 meta if get_config? env = some "dev" then