--- a/Admin/isatest/isatest-makeall Wed Nov 21 14:07:35 2012 +0100
+++ b/Admin/isatest/isatest-makeall Wed Nov 21 15:50:54 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 -o timeout=3600"
+BUILD_ARGS="-v"
NICE="nice"
case $HOSTNAME in
macbroy2 | macbroy6 | macbroy30)
@@ -85,6 +85,15 @@
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
+ case "$SETTINGS" in
+ *sml*)
+ BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
+ ;;
+ *)
+ BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
+ ;;
+ esac
+
# logfile setup
DATE=$(date "+%Y-%m-%d")