Re: buildd could run "make -i" twice on failure

2013-09-08 Thread Ivo De Decker
Daniel, On Sun, Sep 08, 2013 at 10:36:42AM +0200, Daniel Pocock wrote: > > There's no guarantee that "make" is being used for building, and > > it's non-trivial to determine if it is or is not in use, nor how to > > invoke it appropriately. If we want to do it centrally, it would > > be more rel

Re: buildd could run "make -i" twice on failure

2013-09-08 Thread Daniel Pocock
-BEGIN PGP SIGNED MESSAGE- Hash: SHA256 On 08/09/13 01:20, Roger Leigh wrote: > On Sat, Sep 07, 2013 at 11:28:31PM +0200, Daniel Pocock wrote: >> After a build fails on the buildd, it would be really useful to >> have the build run again twice with "make -i" and log the output >> of the

Re: buildd could run "make -i" twice on failure

2013-09-07 Thread Roger Leigh
On Sat, Sep 07, 2013 at 11:28:31PM +0200, Daniel Pocock wrote: > After a build fails on the buildd, it would be really useful to have the > build run again twice with "make -i" and log the output of the second retry What's the main advantage of doing so? To log further errors not seen due to the

buildd could run "make -i" twice on failure

2013-09-07 Thread Daniel Pocock
After a build fails on the buildd, it would be really useful to have the build run again twice with "make -i" and log the output of the second retry Obviously I could hack something like this into debian/rules: make || make -i ; make -i ; exit 1 but it would be nice to have a centrally manag