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

chore: fix test on MacOS

Browse source
This commit is contained in:
tydeu 2023-06-08 14:05:04 -04:00
parent 462d306184
commit 3fb146fad2
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
test/50/test.sh
View file

@ -19,7 +19,8 @@ ${LAKE} build -KleancArgs=-DBAR | tee -a ../produced.out
${LAKE} build
echo "# link args" | tee -a ../produced.out
${LAKE} build -KlinkArgs=-Lbuild/lib | tee -a ../produced.out
# Use `head -n1` to avoid extranous warnings on MacOS with current Lean
${LAKE} build -KlinkArgs=-Lbuild/lib | head -n1 | tee -a ../produced.out
# test
if [ "$OS" = Windows_NT ]; then