Give the script some time to come down.

diff --git a/tools/make-batch b/tools/make-batch
index e41f476e476e8ef9f8cac038e18f727557460b40..d650904ff117784ce7370328f0ed09aa4ea91808 100644 (file)
--- a/tools/make-batch
+++ b/tools/make-batch
@@ -64,6 +64,7 @@ batch_attach() {
 batch_run() {  
        gettoolchain
        $0 build | tee $BATCHLOG
+       sleep 5
        if [ -e $FAILED ]; then
                SUBJECT="Failed :("
        else