From 33b28efdb73a57f308aec9335d4051299fd400f2 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Tue, 5 Oct 2021 21:04:48 -0700
Subject: [PATCH] chore: rm redundant mathlib4 dependency

---
 Lib4/leanbin/lakefile.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/Lib4/leanbin/lakefile.lean b/Lib4/leanbin/lakefile.lean
index af4afbf65..dcb410b9d 100644
--- a/Lib4/leanbin/lakefile.lean
+++ b/Lib4/leanbin/lakefile.lean
@@ -6,11 +6,6 @@ package leanbin {
   libRoots := #[],
   libGlobs := #[],
   dependencies := #[
-  {
-    name := "mathlib",
-    src := Source.git "https://github.com/dselsam/mathlib4.git" "lake" none,
-    dir := FilePath.mk "."
-  },
   {
     name := "mathport",
     src := Source.git "https://github.com/leanprover/mathport.git" "master" none,