From d079f66017ca12d2da8a3bb14fb00630bb840feb Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 23 Dec 2016 17:49:20 +0100 Subject: [PATCH] fix(tests/lean/test_single): work around sed on mac --- tests/lean/test_single.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index dfceaab9c0..826b55d4b1 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -22,11 +22,11 @@ fi echo "-- testing $f" "$LEAN" -Dpp.colors=false -Dpp.unicode=true -j0 "$ff" &> "$f.produced.out" -sed -i 's|does\\not\\exist|does/not/exist|' "$f.produced.out" -sed -i "/warning: imported file uses 'sorry'/d" "$f.produced.out" -sed -i "/warning: using 'sorry'/d" "$f.produced.out" -sed -i "/failed to elaborate theorem/d" "$f.produced.out" -sed -i "s|^$ff|$f|" "$f.produced.out" +sed -i.tmp 's|does\\not\\exist|does/not/exist|' "$f.produced.out" +sed -i.tmp "/warning: imported file uses 'sorry'/d" "$f.produced.out" +sed -i.tmp "/warning: using 'sorry'/d" "$f.produced.out" +sed -i.tmp "/failed to elaborate theorem/d" "$f.produced.out" +sed -i.tmp "s|^$ff|$f|" "$f.produced.out" if test -f "$f.expected.out"; then if diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"; then echo "-- checked"