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

test: increase sleep in 44

Browse source
This commit is contained in:
tydeu 2022-12-02 14:20:58 -05:00
parent 25ab266a2e
commit c60ccdc974
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
test/44/test.sh
View file

@ -7,7 +7,7 @@ LAKE=${LAKE:-../../build/bin/lake}
$LAKE new hello
$LAKE -d hello build
sleep 0.1 # for some reason, delay needed for `--old` rebuild consistency
sleep 0.5 # for some reason, delay needed for `--old` rebuild consistency
echo 'def hello := "old"' > hello/Hello.lean
$LAKE -d hello build --old | tee produced.out
echo 'def hello := "normal"' > hello/Hello.lean