widelands-dev team mailing list archive

[Teppo Mäenpää <tm@xxxxxx>]

Got the random error, again. I guess bunnybot will not merge now.

If we cannot alter the way the infra works, would it be possible to work around?

What do the scripts look like ? If the errors are truly random, one could try
command || (sleep 10 && command) || $(sleep 10 && command)

or, in this case, 
git clone $ADDR || (rm -Rf $repodir || true ; sleep 10 && git clone $ADDR )) <and so on>

-- 
https://code.launchpad.net/~widelands-dev/widelands/bug-1574379-forester-wit/+merge/336068
Your team Widelands Developers is subscribed to branch lp:~widelands-dev/widelands/bug-1574379-forester-wit.