# HG changeset patch
# User wenzelm
# Date 1353414444 -3600
# Node ID e69db78b36d68113b2962a108ac8cb72b6b31a37
# Parent  599c935aac828ad76a193e4e455397ebf5ea4457
global default for session timeout;

diff -r 599c935aac82 -r e69db78b36d6 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Mon Nov 19 22:34:17 2012 +0100
+++ b/Admin/isatest/isatest-makeall	Tue Nov 20 13:27:24 2012 +0100
@@ -47,7 +47,7 @@
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
 # build args and nice setup for different target platforms
-BUILD_ARGS="-v"
+BUILD_ARGS="-v -o timeout=3600"
 NICE="nice"
 case $HOSTNAME in
     macbroy2 | macbroy6 | macbroy30)