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

chore: fix test

Browse source
This commit is contained in:
tydeu 2022-06-16 02:24:46 -04:00
parent eb7979b332
commit 61926bbb32
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
test/75/test.sh
View file

@ -5,6 +5,7 @@ LAKE=${LAKE:-../../../build/bin/lake}
cd foo
rm -rf build
mkdir -p Foo
echo $'def a := "a"' > Foo/Test.lean
echo $'import Foo.Test def hello := a' > Foo.lean
${LAKE} build