diff -r 8d2251b9a200 -r aaf276a28551 Admin/isatest/isatest-makeall
--- 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")