# 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)