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"