From 2866824b51536fd39fd9f921c26d33579c248fe2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Oct 2019 17:35:05 +0200
Subject: [PATCH] test: capture stderr as well

This might or might not give more information on randomly failing tests on CI
/cc @leodemoura
---
 tests/bench/test_single.sh              | 2 +-
 tests/compiler/test_single.sh           | 2 +-
 tests/compiler/test_single_interpret.sh | 2 +-
 tests/lean/test_single.sh               | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/bench/test_single.sh b/tests/bench/test_single.sh
index fa6f0890b9..6c84ad3c60 100755
--- a/tests/bench/test_single.sh
+++ b/tests/bench/test_single.sh
@@ -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
diff --git a/tests/compiler/test_single.sh b/tests/compiler/test_single.sh
index 68091b9fcf..bcf556e804 100755
--- a/tests/compiler/test_single.sh
+++ b/tests/compiler/test_single.sh
@@ -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
diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh
index 5f872df372..118c637fa6 100755
--- a/tests/compiler/test_single_interpret.sh
+++ b/tests/compiler/test_single_interpret.sh
@@ -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
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index 8a3edf2438..799d951a4f 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -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"