max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: adjustment for lake update behavior change

Browse source
This commit is contained in:
tydeu 2023-10-30 19:33:34 -04:00 • committed by Mac Malone
parent 793329fd56
commit 72fdddfed3
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/lake/tests/depTree/test.sh
View file

@ -129,14 +129,13 @@ sed_i 's/third commit/fourth commit/' A.lean
git commit -am 'fourth commit in a'
popd
pushd d
# d: no require c
sed_i '/require c/d' lakefile.lean
# d: b@1 -> b@2 => a@1 -> a@3
$LAKE update b -v
# test 119: pickup a@3 and not a@4
grep 'third commit in a' lake-packages/a/A.lean
# test the removal of `c` from the manifest
grep "\"c\"" lake-manifest.json
sed_i '/require c/d' lakefile.lean
$LAKE update c -v
! grep "\"c\"" lake-manifest.json
grep "\"c\"" lake-manifest.json && false || true
popd