test: capture stderr as well
This might or might not give more information on randomly failing tests on CI /cc @leodemoura
This commit is contained in:
parent
0c3c5bf82f
commit
2866824b51
4 changed files with 4 additions and 4 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue