update grid5000.sh

DIVERSIFY-project · Dec 17, 2013 · 91ed480 · 91ed480
1 parent 8969542
commit 91ed480
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/grid5000.sh b/grid5000.sh
@@ -4,7 +4,7 @@ git pull
 mvn clean package
 
 n=$RANDOM
-sleep $(( r %= 120 ))
+sleep $(( r %= 300 ))
 
 rm -rf repo/diversify-exp
 java -jar target/Diversify-statements-1.0-SNAPSHOT-jar-with-dependencies.jar git repo