chore: rm redundant mathlib4 dependency

leanprover-community · Oct 6, 2021 · 33b28ef · 33b28ef
1 parent fea2b7b
commit 33b28ef
Showing 1 changed file with 0 additions and 5 deletions.
diff --git 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,