chore: fix tests/online

leanprover · Oct 19, 2024 · 5e8b29e · 5e8b29e
1 parent e548d57
commit 5e8b29e
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh
@@ -11,13 +11,13 @@ export ELAN_TOOLCHAIN=test
   grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
 
 ./clean.sh
-$LAKE -f git.toml update
+$LAKE -f git.toml update --keep-toolchain
 # Test that barrels are not fetched for non-Reservoir dependencies
 $LAKE -v -f git.toml build @Cli:extraDep |
   grep --color "Cli:optBarrel" && exit 1 || true
 
 ./clean.sh
-$LAKE -f barrel.lean update
+$LAKE -f barrel.lean update --keep-toolchain
 # Test that a barrel is not fetched for an unbuilt dependency
 $LAKE -v -f barrel.lean build @test:extraDep |
   grep --color "Cli:optBarrel" && exit 1 || true
@@ -53,11 +53,11 @@ LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
   $LAKE -f barrel.lean build Cli --no-build
 
 ./clean.sh
-$LAKE -f require.lean update -v
+$LAKE -f require.lean update -v --keep-toolchain
 test -d .lake/packages/doc-gen4
 $LAKE -f require.lean resolve-deps  # validate manifest
 
 ./clean.sh
-$LAKE -f require.toml update  v
+$LAKE -f require.toml update -v --keep-toolchain
 test -d .lake/packages/doc-gen4
 $LAKE -f require.toml resolve-deps  # validate manifest