remove unnecessary line in scripts/update_mathlib.sh

fpvandoorn · Nov 8, 2024 · 6f3fb43 · 6f3fb43
1 parent 92592f5
commit 6f3fb43
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh
@@ -3,4 +3,3 @@
 # Update mathlib and the lean toolchain.
 curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
 lake -R -Kenv=dev update # The `-R -Kenv=dev` is making sure we also update doc-gen and other dependencies
-lake exe cache get