Index: tools/batch-cmd
===================================================================
--- tools/batch-cmd	(revision 9955)
+++ tools/batch-cmd	(revision 9956)
@@ -13,5 +13,5 @@
 
 for HOST in $HOSTS; do
-  ssh -o ConnectTimeout=3 root@$HOST.wleiden.net. $CMD > $PREFIX-$HOST.txt &
+  ssh -o ConnectTimeout=3 -o BatchMode=yes root@$HOST.wleiden.net. $CMD > $PREFIX-$HOST.txt &
 done