diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh index 16288a47ad..7859544f29 100755 --- a/tests/lean/interactive/test_single.sh +++ b/tests/lean/interactive/test_single.sh @@ -32,7 +32,7 @@ echo "-- testing $f" OUTPUT="$("$LEAN" -j0 -D pp.unicode=true --server < "$f")" # make paths system-independent if [[ "$OSTYPE" == "msys" ]]; then - echo "$OUTPUT" | sed "s|$ROOT_PATH_NORMALIZED||g" | sed 's|\\\\|/|g' > "$f.produced.out" + echo "$OUTPUT" | grep -v '"response":"current_tasks"' | sed "s|$ROOT_PATH_NORMALIZED||g" | sed 's|\\\\|/|g' > "$f.produced.out" else OUTPUT=${OUTPUT//$ROOT_PATH_NORMALIZED/} echo "$OUTPUT" > "$f.produced.out"