Do not use tee on batch build any more.

diff --git a/tools/make-batch b/tools/make-batch
index c12404c8553e949ec612b57c6344cc4585ca4318..4187eb08f5777e8c8db392df48d3ad468c848c2e 100644 (file)
--- a/tools/make-batch
+++ b/tools/make-batch
@@ -47,9 +47,9 @@ batch_attach() {
 ###############################################################################
 batch_run() {
        gettoolchain
-       $0 build | $BASEDIR/tools/tee $BATCHLOG
-       sleep 5
-       if [ -e $FAILED ]; then
+       $0 build &> $BATCHLOG
+       sleep 30
+       if [ -e "$FAILED" ]; then
                SUBJECT="Failed :("
        else
                SUBJECT="Success!"