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

chore: test 44 shell script fixes

Browse source
This commit is contained in:
tydeu 2022-08-03 00:50:34 -04:00
parent 5b81042614
commit 19afb95dd7
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
test/44/test.sh
View file

@ -12,9 +12,9 @@ echo 'def hello := "old"' > hello/Hello.lean
$LAKE -d hello build --old | tee produced.out
echo 'def hello := "normal"' > hello/Hello.lean
$LAKE -d hello build | tee -a produced.out
if [ "`uname`" = Darwin ]; then
sed -i '' 's/.exe//g' produced.out
else
if [ "$OS" = Windows_NT ]; then
sed -i 's/.exe//g' produced.out
diff --strip-trailing-cr expected.out produced.out
else
diff expected.out produced.out
fi
diff expected.out produced.out