From d7b2dcf7e54436579771decd223f8b1a7718edb4 Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 3 Aug 2022 00:50:34 -0400 Subject: [PATCH] chore: test 44 shell script fixes --- test/44/test.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/44/test.sh b/test/44/test.sh index 152f3cd..3128582 100755 --- a/test/44/test.sh +++ b/test/44/test.sh @@ -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