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

chore(tests/lean/interactive/test_single): ignore progress responses

Browse source
This commit is contained in:
Sebastian Ullrich 2016-12-27 16:16:00 +01:00 • committed by Leonardo de Moura
parent 33ec940604
commit b10ebade8c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/test_single.sh
View file

@ -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"