chore: revert "test: capture stderr as well"

This reverts commit 2866824b51.
This commit is contained in:
Sebastian Ullrich 2019-10-29 19:55:19 +01:00
parent a43a225013
commit 5ce9ca81da
4 changed files with 4 additions and 4 deletions

View file

@ -19,7 +19,7 @@ fi
./compile.sh "$ff" || exit 1
[ -f "$ff.args" ] && args=$(cat "$ff.args")
"./$ff.out" $args &> "$ff.produced.out"
"./$ff.out" $args > "$ff.produced.out"
if [ $? -ne 0 ]; then
echo "Failed to execute $ff.out"
exit 1

View file

@ -37,7 +37,7 @@ if [ $? -ne 0 ]; then
exit 1
fi
"./$ff.out" &> "$ff.produced.out"
"./$ff.out" > "$ff.produced.out"
if [ $? -ne 0 ]; then
echo "Failed to execute $ff.out"
exit 1

View file

@ -25,7 +25,7 @@ if diff --color --help >/dev/null 2>&1; then
DIFF="diff --color";
fi
$LEAN --run "$ff" &> "$ff.produced.out"
$LEAN --run "$ff" > "$ff.produced.out"
if [ $? -ne 0 ]; then
echo "Failed to execute $ff"
exit 1

View file

@ -26,7 +26,7 @@ if diff --color --help >/dev/null 2>&1; then
fi
echo "-- testing $f"
"$LEAN" "$ff" | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" &> "$f.produced.out"
"$LEAN" "$ff" | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out"
if test -f "$f.expected.out"; then
if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
echo "-- checked"