From 1f16421118b0e679bc9b0d8a09b48535544977e3 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Thu, 14 Dec 2023 23:52:43 +0000
Subject: [PATCH] try removing LeanCopilot?

---
 lakefile.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index e91024c9..0feda4a9 100644
--- 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