Use reservoir require for mathlib.

checkdecls is not on reservoir
leanprover-community · Aug 1, 2024 · 7260949 · 7260949
1 parent 9567b65
commit 7260949
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lakefile.toml b/lakefile.toml
@@ -8,7 +8,7 @@ relaxedAutoImplicit = false
 
 [[require]]
 name = "mathlib"
-git = "https://github.com/leanprover-community/mathlib4.git"
+scope = "leanprover-community"
 
 [[require]]
 name = "checkdecls"